Seq 📖 | CompOp | 39 mathmath: GenContFract.IntFractPair.seq1_fst_eq_of, Tactic.ComputeAsymptotics.Seq.dist_cons_nil, Seq.cons_injective2, Tactic.ComputeAsymptotics.Seq.instBoundedSpaceSeq, Seq.join_cons_cons, Tactic.ComputeAsymptotics.Seq.FriendlyOperation.ite, Seq.toList_nil, Tactic.ComputeAsymptotics.Seq.dist_cons_cons_eq_one, Tactic.ComputeAsymptotics.Seq.FriendlyOperation.exists_fixed_point, Seq.cons_left_injective, Tactic.ComputeAsymptotics.Seq.dist_eq_one_of_head, Tactic.ComputeAsymptotics.Seq.FriendlyOperation.id, Tactic.ComputeAsymptotics.Seq.dist_cons_cons, Tactic.ComputeAsymptotics.Seq.dist_eq_two_inv_pow, Tactic.ComputeAsymptotics.Seq.dist_nil_cons, Seq.cons_right_injective, Seq.mem_iff_exists_get?, Tactic.ComputeAsymptotics.Seq.FriendlyOperation.comp, Seq.notMem_nil, Seq.join_cons_nil, Seq.get?_mem, GenContFract.IntFractPair.get?_seq1_eq_succ_get?_stream, Seq.corec_eq, Seq1.join_cons, Tactic.ComputeAsymptotics.Seq.instCompleteSpaceSeq, GenContFract.of_h_eq_intFractPair_seq1_fst_b, Seq.join_cons, Seq1.map_pair, Seq1.join_nil, Seq.mem_cons, Seq.destruct_cons, GenContFract.of_terminatedAt_iff_intFractPair_seq1_terminatedAt, Tactic.ComputeAsymptotics.Seq.FriendlyOperation.dist_le, Tactic.ComputeAsymptotics.Seq.dist_eq_half_of_head, Seq.head_eq_destruct, Tactic.ComputeAsymptotics.Seq.dist_le_one, Seq.mem_cons_iff, Seq.instLawfulFunctor, Seq.ofList_injective
|