Results for fold 1 Results for lemma ex_maxn_subproof: : exists i, P (m - i) FAILURE! Tactics applied: 10000 Original Proof: [by case: exP => i Pi; exists (m - i); rewrite subKn ?ubP.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 485 Number of failed tactic applications: 9516 Results for lemma lt0n: n : (0 < n) = (n != 0) SUCCESS! Proof Found in EFSM: by case: n. Tactics applied: 92 Original Proof: [by case: n.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 1 Number of failed tactic applications: 91 Results for lemma minnCA: : left_commutative minn FAILURE! Tactics applied: 10000 Original Proof: [by move=> m n p; rewrite !minnA (minnC n).] Proof search time: 0 min, 29 sec Number of successful tactic applications: 3929 Number of failed tactic applications: 6072 Results for lemma le_irrelevance: m n le_mn1 le_mn2 : le_mn1 = le_mn2 :> (m <= n)%coq_nat FAILURE! Tactics applied: 338 Original Proof: [elim: {n}n.+1 {-1}n (erefl n.+1) => // n IHn _ [<-] in le_mn1 le_mn2 *. pose def_n2 := erefl n; transitivity (eq_ind _ _ le_mn2 _ def_n2) => //. move def_n1: {1 4 5 7}n le_mn1 le_mn2 def_n2 => n1 le_mn1. case: n1 / le_mn1 def_n1 => [|n1 le_mn1] def_n1 [|n2 le_mn2] def_n2. - by rewrite [def_n2]eq_axiomK. - by move/leP: (le_mn2); rewrite -{1}def_n2 ltnn. - by move/leP: (le_mn1); rewrite {1}def_n2 ltnn. case: def_n2 (def_n2) => ->{n2} def_n2 in le_mn2 *. by rewrite [def_n2]eq_axiomK /=; congr le_S; exact: IHn.] Proof search time: 0 min, 1 sec Number of successful tactic applications: 0 Number of failed tactic applications: 338 Results for lemma addSn: m n : m.+1 + n = (m + n).+1 SUCCESS! Proof Found in EFSM: split ; Tactics applied: 37 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 2 Number of failed tactic applications: 35 Results for lemma leq_total: m n : (m <= n) || (m >= n) SUCCESS! Proof Found in EFSM: elim : m n => [|m IHm] [|n] //; exact : IHm n. Tactics applied: 372 Original Proof: [by rewrite -implyNb -ltnNge; apply/implyP; exact: ltnW.] Shorter Proof Found? yes Proof reused from doubleB proof search time: 0 min, 1 sec Number of successful tactic applications: 4 Number of failed tactic applications: 368 Results for lemma leq_eqVlt: m n : (m <= n) = (m == n) || (m < n) SUCCESS! Proof Found in EFSM: elim : m n => [|m IHm] [|n] //; exact : IHm n. Tactics applied: 373 Original Proof: [elim: m n => [|m IHm] [|n] //; exact: IHm n.] Shorter Proof Found? no Proof reused from doubleB proof search time: 0 min, 1 sec Number of successful tactic applications: 7 Number of failed tactic applications: 366 Results for lemma leq_exp2r: m n e : e > 0 -> (m ^ e <= n ^ e) = (m <= n) FAILURE! Tactics applied: 10000 Original Proof: [by move=> e_gt0; rewrite leqNgt ltn_exp2r // -leqNgt.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 724 Number of failed tactic applications: 9277 Results for lemma uphalf_double: n : uphalf n.*2 = n SUCCESS! Proof Found in EFSM: by elim: n => //= n ->. Tactics applied: 123 Original Proof: [by elim: n => //= n ->.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 1 Number of failed tactic applications: 122 Results for lemma eqn_add2l: p m n : (p + m == p + n) = (m == n) SUCCESS! Proof Found in EFSM: by elim: p. Tactics applied: 140 Original Proof: [by elim: p.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 4 Number of failed tactic applications: 136 Results for lemma mulnbr: (b : bool) n : n * b = (if b then n else 0) FAILURE! Tactics applied: 339 Original Proof: [by rewrite mulnC mulnbl.] Proof search time: 0 min, 1 sec Number of successful tactic applications: 0 Number of failed tactic applications: 339 Results for lemma addn2: m : m + 2 = m.+2 SUCCESS! Proof Found in EFSM: exact : addnC. Tactics applied: 47 Original Proof: [by rewrite addnC.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 1 Number of failed tactic applications: 46 Results for lemma addnAC: : right_commutative addn FAILURE! Tactics applied: 10000 Original Proof: [by move=> m n p; rewrite -!addnA (addnC n).] Proof search time: 0 min, 13 sec Number of successful tactic applications: 405 Number of failed tactic applications: 9596 Results for lemma ltn_exp2l: m n1 n2 : 1 < m -> (m ^ n1 < m ^ n2) = (n1 < n2) FAILURE! Tactics applied: 10000 Original Proof: [by move=> m_gt1; rewrite !ltnNge leq_exp2l.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 814 Number of failed tactic applications: 9187 Results for lemma exp0n: n : 0 < n -> 0 ^ n = 0 SUCCESS! Proof Found in EFSM: by case: n => [|[|[]]]. Tactics applied: 94 Original Proof: [by case: n => [|[]].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 15 Number of failed tactic applications: 79 Results for lemma expn_eq0: m e : (m ^ e == 0) = (m == 0) && (e > 0) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite !eqn0Ngt expn_gt0 negb_or -lt0n.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 704 Number of failed tactic applications: 9297 Results for lemma leq_maxl: m n : m <= maxn m n FAILURE! Tactics applied: 10000 Original Proof: [by rewrite leq_max leqnn.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 1173 Number of failed tactic applications: 8828 Results for lemma ltnW: m n : m < n -> m <= n SUCCESS! Proof Found in EFSM: move => Hmn; exact : leq_trans. Tactics applied: 375 Original Proof: [exact: leq_trans.] Shorter Proof Found? no Proof reused from leq_ltn_trans proof search time: 0 min, 1 sec Number of successful tactic applications: 22 Number of failed tactic applications: 353 Results for lemma odd_double_half: n : odd n + n./2.*2 = n FAILURE! Tactics applied: 338 Original Proof: [by elim: n => //= n {3}<-; rewrite uphalf_half doubleD; case (odd n).] Proof search time: 0 min, 1 sec Number of successful tactic applications: 0 Number of failed tactic applications: 338 Results for lemma geq_minr: m n : minn m n <= n FAILURE! Tactics applied: 10000 Original Proof: [by rewrite minnC geq_minl.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 1209 Number of failed tactic applications: 8792 Results for lemma leP: m n : reflect (m <= n)%coq_nat (m <= n) FAILURE! Tactics applied: 415 Original Proof: [apply: (iffP idP); last by elim: n / => // n _ /leq_trans->. elim: n => [|n IHn]; first by case: m. by rewrite leq_eqVlt ltnS => /predU1P[<- // | /IHn]; right.] Proof search time: 0 min, 1 sec Number of successful tactic applications: 3 Number of failed tactic applications: 412 Results for lemma geq_min: m n1 n2 : (m >= minn n1 n2) = (m >= n1) || (m >= n2) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -ltnS gtn_min.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 561 Number of failed tactic applications: 9440 Results for lemma ltn_expl: m n : 1 < m -> n < m ^ n FAILURE! Tactics applied: 10000 Original Proof: [move=> m_gt1; elim: n => //= n; rewrite -(leq_pmul2l (ltnW m_gt1)) expnS. by apply: leq_trans; exact: ltn_Pmull.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 1058 Number of failed tactic applications: 8943 Results for lemma addnACA: : interchange addn addn FAILURE! Tactics applied: 10000 Original Proof: [by move=> m n p q; rewrite -!addnA (addnCA n).] Proof search time: 0 min, 13 sec Number of successful tactic applications: 424 Number of failed tactic applications: 9577 Results for lemma mulnDr: : right_distributive muln addn FAILURE! Tactics applied: 10000 Original Proof: [by move=> m n1 n2; rewrite !(mulnC m) mulnDl.] Proof search time: 0 min, 16 sec Number of successful tactic applications: 559 Number of failed tactic applications: 9442 Results for lemma mono_leqif: f : {mono f : m n / m <= n} -> forall m n C, (f m <= f n ?= iff C) = (m <= n ?= iff C) FAILURE! Tactics applied: 10000 Original Proof: [by move=> f_mono m n C; rewrite /leqif !eqn_leq !f_mono.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 489 Number of failed tactic applications: 9512 Results for lemma addE: : add =2 addn FAILURE! Tactics applied: 10000 Original Proof: [by elim=> //= n IHn m; rewrite IHn addSnnS.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 789 Number of failed tactic applications: 9212 Results for lemma minn_maxl: : left_distributive minn maxn FAILURE! Tactics applied: 10000 Original Proof: [by move=> m1 m2 n; rewrite maxn_minr !maxn_minl -minnA maxnn (maxnC _ n) !maxnK.] Proof search time: 0 min, 29 sec Number of successful tactic applications: 4011 Number of failed tactic applications: 5990 Results for lemma ltn_add2l: p m n : (p + m < p + n) = (m < n) SUCCESS! Proof Found in EFSM: by elim: p. Tactics applied: 140 Original Proof: [by rewrite -addnS; exact: leq_add2l.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 4 Number of failed tactic applications: 136 Results for lemma ltn_pmul2r: m n1 n2 : 0 < m -> (n1 * m < n2 * m) = (n1 < n2) FAILURE! Tactics applied: 10000 Original Proof: [by move/prednK <-; rewrite ltn_mul2r.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 841 Number of failed tactic applications: 9160 Results for lemma subSS: n m : m.+1 - n.+1 = m - n SUCCESS! Proof Found in EFSM: split ; Tactics applied: 37 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 2 Number of failed tactic applications: 35 Results for lemma addnK: n : cancel (addn^~ n) (subn^~ n) FAILURE! Tactics applied: 801 Original Proof: [by move=> m; rewrite /= (addnC m) addKn.] Proof search time: 0 min, 1 sec Number of successful tactic applications: 14 Number of failed tactic applications: 787 Results for lemma double_gt0: n : (0 < n.*2) = (0 < n) SUCCESS! Proof Found in EFSM: by case: n. Tactics applied: 92 Original Proof: [by case: n.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 1 Number of failed tactic applications: 91 Results for lemma eq_iterop: n op op' : op =2 op' -> iterop n op =2 iterop n op' FAILURE! Tactics applied: 1131 Original Proof: [by move=> eq_op x; apply: eq_iteri; case.] Proof search time: 0 min, 2 sec Number of successful tactic applications: 22 Number of failed tactic applications: 1109 Results for lemma eqn_leq: m n : (m == n) = (m <= n <= m) SUCCESS! Proof Found in EFSM: elim : m n => [|m IHm] [|n] //; exact : IHm n. Tactics applied: 372 Original Proof: [elim: m n => [|m IHm] [|n] //; exact: IHm n.] Shorter Proof Found? no Proof reused from doubleB proof search time: 0 min, 1 sec Number of successful tactic applications: 5 Number of failed tactic applications: 367 Results for fold 2 Results for lemma eqn_mul2l: m n1 n2 : (m * n1 == m * n2) = (m == 0) || (n1 == n2) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite eqn_leq !leq_mul2l -orb_andr -eqn_leq.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 1030 Number of failed tactic applications: 8971 Results for lemma addn_maxr: : right_distributive addn maxn FAILURE! Tactics applied: 10000 Original Proof: [by move=> m n1 n2; rewrite !(addnC m) addn_maxl.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 1668 Number of failed tactic applications: 8333 Results for lemma sqrnD_sub: m n : n <= m -> (m + n) ^ 2 - 4 * (m * n) = (m - n) ^ 2 FAILURE! Tactics applied: 10000 Original Proof: [move=> le_nm; rewrite -[4]/(2 * 2) -mulnA mul2n -addnn subnDA. by rewrite sqrnD addnK sqrn_sub.] Proof search time: 0 min, 33 sec Number of successful tactic applications: 821 Number of failed tactic applications: 9180 Results for lemma uphalf_half: n : uphalf n = odd n + n./2 FAILURE! Tactics applied: 10000 Original Proof: [by elim: n => //= n ->; rewrite addnA addn_negb.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 1033 Number of failed tactic applications: 8968 Results for lemma maxnK: m n : minn (maxn m n) m = m FAILURE! Tactics applied: 10000 Original Proof: [exact/minn_idPr/leq_maxl.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 389 Number of failed tactic applications: 9612 Results for lemma eqn_pmul2r: m n1 n2 : 0 < m -> (n1 * m == n2 * m) = (n1 == n2) FAILURE! Tactics applied: 10000 Original Proof: [by move/prednK <-; rewrite eqn_mul2r.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 584 Number of failed tactic applications: 9417 Results for lemma mulSn: m n : m.+1 * n = n + m * n SUCCESS! Proof Found in EFSM: constructor. Tactics applied: 5 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 4 Number of failed tactic applications: 1 Results for lemma leq_mul2l: m n1 n2 : (m * n1 <= m * n2) = (m == 0) || (n1 <= n2) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite {1}/leq -mulnBr muln_eq0.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 1127 Number of failed tactic applications: 8874 Results for lemma maxnAC: : right_commutative maxn FAILURE! Tactics applied: 10000 Original Proof: [by move=> m n p; rewrite !maxnE -!addnA !subnDA -!maxnE maxnC.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 1127 Number of failed tactic applications: 8874 Results for lemma ltnSn: n : n < n.+1 SUCCESS! Proof Found in EFSM: rewrite ?expn1 // ltn_mul // IHe. Tactics applied: 95 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 7 Number of failed tactic applications: 88 Results for lemma eq_ex_minn: P Q exP exQ : P =1 Q -> @ex_minn P exP = @ex_minn Q exQ FAILURE! Tactics applied: 10000 Original Proof: [move=> eqPQ; case: ex_minnP => m1 Pm1 m1_lb; case: ex_minnP => m2 Pm2 m2_lb. by apply/eqP; rewrite eqn_leq m1_lb (m2_lb, eqPQ) // -eqPQ.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 366 Number of failed tactic applications: 9635 Results for lemma leqP: m n : leq_xor_gtn m n (m <= n) (n < m) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite ltnNge; case le_mn: (m <= n); constructor; rewrite // ltnNge le_mn.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 483 Number of failed tactic applications: 9518 Results for lemma doubleS: n : n.+1.*2 = n.*2.+2 SUCCESS! Proof Found in EFSM: constructor. Tactics applied: 5 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 2 Results for lemma subnSK: m n : m < n -> (n - m.+1).+1 = n - m FAILURE! Tactics applied: 10000 Original Proof: [by move/subSn.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 1008 Number of failed tactic applications: 8993 Results for lemma leq_maxr: m n : n <= maxn m n FAILURE! Tactics applied: 10000 Original Proof: [by rewrite maxnC leq_maxl.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 618 Number of failed tactic applications: 9383 Results for lemma ltn_mul: m1 m2 n1 n2 : m1 < n1 -> m2 < n2 -> m1 * m2 < n1 * n2 FAILURE! Tactics applied: 10000 Original Proof: [move=> lt_mn1 lt_mn2; apply (@leq_ltn_trans (m1 * n2)). by rewrite leq_mul2l orbC ltnW. by rewrite ltn_pmul2r // (leq_trans _ lt_mn2).] Proof search time: 0 min, 23 sec Number of successful tactic applications: 946 Number of failed tactic applications: 9055 Results for lemma eq_leq: m n : m = n -> m <= n SUCCESS! Proof Found in EFSM: by elim. Tactics applied: 163 Original Proof: [by move->.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 23 Number of failed tactic applications: 140 Results for lemma ltn0: n : n < 0 = false SUCCESS! Proof Found in EFSM: constructor. Tactics applied: 5 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 2 Results for lemma leqif_mul: m1 n1 C1 m2 n2 C2 : m1 <= n1 ?= iff C1 -> m2 <= n2 ?= iff C2 -> m1 * m2 <= n1 * n2 ?= iff (n1 * n2 == 0) || (C1 && C2) FAILURE! Tactics applied: 10000 Original Proof: [move=> le1 le2; case: posnP => [n12_0 | ]. rewrite n12_0; move/eqP: n12_0 {le1 le2}le1.1 le2.1; rewrite muln_eq0. by case/orP=> /eqP->; case: m1 m2 => [|m1] [|m2] // _ _; rewrite ?muln0; exact/leqif_refl. rewrite muln_gt0 => /andP[n1_gt0 n2_gt0]. have [m2_0 | m2_gt0] := posnP m2. apply/leqifP; rewrite -le2 andbC eq_sym eqn_leq leqNgt m2_0 muln0. by rewrite muln_gt0 n1_gt0 n2_gt0. have mono_n1 := leq_pmul2l n1_gt0; have mono_m2 := leq_pmul2r m2_gt0. rewrite -(mono_leqif mono_m2) in le1; rewrite -(mono_leqif mono_n1) in le2. exact: leqif_trans le1 le2.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 701 Number of failed tactic applications: 9300 Results for lemma minnC: : commutative minn FAILURE! Tactics applied: 10000 Original Proof: [by move=> m n; rewrite /minn; case ltngtP.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 1587 Number of failed tactic applications: 8414 Results for lemma doubleE: : double = double_rec SUCCESS! Proof Found in EFSM: constructor. Tactics applied: 5 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 4 Results for lemma double_eq0: n : (n.*2 == 0) = (n == 0) SUCCESS! Proof Found in EFSM: by case: n. Tactics applied: 151 Original Proof: [by case: n.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 9 Number of failed tactic applications: 142 Results for lemma nat_of_mul_bin: b1 b2 : (b1 * b2)%num = b1 * b2 :> nat FAILURE! Tactics applied: 10000 Original Proof: [case: b1 b2 => [|p] [|q] //=; elim: p => [p IHp|p IHp|] /=; by rewrite ?(mul1n, nat_of_addn_gt0, mulSn) //= !natTrecE IHp doubleMl.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 292 Number of failed tactic applications: 9709 Results for lemma iter_addn_0: m n : iter n (addn m) 0 = m * n FAILURE! Tactics applied: 10000 Original Proof: [by rewrite iter_addn addn0.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 606 Number of failed tactic applications: 9395 Results for lemma leqif_trans: m1 m2 m3 C12 C23 : m1 <= m2 ?= iff C12 -> m2 <= m3 ?= iff C23 -> m1 <= m3 ?= iff C12 && C23 FAILURE! Tactics applied: 10000 Original Proof: [move=> ltm12 ltm23; apply/leqifP; rewrite -ltm12. case eqm12: (m1 == m2). by rewrite (eqP eqm12) ltn_neqAle !ltm23 andbT; case C23. by rewrite (@leq_trans m2) ?ltm23 // ltn_neqAle eqm12 ltm12.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 594 Number of failed tactic applications: 9407 Results for lemma leq_pmull: m n : n > 0 -> m <= n * m FAILURE! Tactics applied: 10000 Original Proof: [by move/prednK <-; exact: leq_addr.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 889 Number of failed tactic applications: 9112 Results for lemma expnM: m n1 n2 : m ^ (n1 * n2) = (m ^ n1) ^ n2 FAILURE! Tactics applied: 10000 Original Proof: [elim: n1 => [|n1 IHn]; first by rewrite exp1n. by rewrite expnD expnS expnMn IHn.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 1005 Number of failed tactic applications: 8996 Results for lemma subnDl: p m n : (p + m) - (p + n) = m - n SUCCESS! Proof Found in EFSM: by elim: p. Tactics applied: 200 Original Proof: [by elim: p.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 12 Number of failed tactic applications: 188 Results for lemma ltn_Pmulr: m n : 1 < n -> 0 < m -> m < m * n FAILURE! Tactics applied: 10000 Original Proof: [by move=> lt1n m_gt0; rewrite mulnC ltn_Pmull.] Proof search time: 0 min, 30 sec Number of successful tactic applications: 1046 Number of failed tactic applications: 8955 Results for lemma mulnC: : commutative muln FAILURE! Tactics applied: 10000 Original Proof: [by move=> m n; elim: m => [|m]; rewrite (muln0, mulnS) // mulSn => ->.] Proof search time: 0 min, 16 sec Number of successful tactic applications: 957 Number of failed tactic applications: 9044 Results for lemma leq_subr: m n : n - m <= n FAILURE! Tactics applied: 10000 Original Proof: [by rewrite leq_subLR leq_addl.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 587 Number of failed tactic applications: 9414 Results for lemma subn2: n : (n - 2)%N = n.-2 FAILURE! Tactics applied: 10000 Original Proof: [by case: n => [|[|[]]].] Proof search time: 0 min, 16 sec Number of successful tactic applications: 1241 Number of failed tactic applications: 8760 Results for lemma subnS: m n : m - n.+1 = (m - n).-1 FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -addn1 subnDA subn1.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 520 Number of failed tactic applications: 9481 Results for lemma ltn_add2r: p m n : (m + p < n + p) = (m < n) FAILURE! Tactics applied: 10000 Original Proof: [exact: leq_add2r p m.+1 n.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 725 Number of failed tactic applications: 9276 Results for lemma doubleE: : double =1 doublen ERROR! Error: The reference doublen was not found in the current environment. Original Proof: [by [].] Proof effort time: 0 min, 0 sec Results for fold 3 Results for lemma ltn0Sn: n : 0 < n.+1 SUCCESS! Proof Found in EFSM: split ; Tactics applied: 50 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 47 Results for lemma eq_iteri: f f' : f =2 f' -> forall n, iteri n f =1 iteri n f' FAILURE! Tactics applied: 10000 Original Proof: [by move=> eq_f n x; elim: n => //= n ->; rewrite eq_f.] Proof search time: 0 min, 13 sec Number of successful tactic applications: 650 Number of failed tactic applications: 9351 Results for lemma leq_sqr: m n : (m ^ 2 <= n ^ 2) = (m <= n) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite leq_exp2r.] Proof search time: 0 min, 31 sec Number of successful tactic applications: 619 Number of failed tactic applications: 9382 Results for lemma odd_sub: m n : n <= m -> odd (m - n) = odd m (+) odd n FAILURE! Tactics applied: 10000 Original Proof: [by move=> le_nm; apply: (@canRL bool) (addbK _) _; rewrite -odd_add subnK.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 488 Number of failed tactic applications: 9513 Results for lemma leqifP: m n C : reflect (m <= n ?= iff C) (if C then m == n else m < n) FAILURE! Tactics applied: 10000 Original Proof: [rewrite ltn_neqAle; apply: (iffP idP) => [|lte]; last by rewrite !lte; case C. by case C => [/eqP-> | /andP[/negPf]]; split=> //; exact: eqxx.] Proof search time: 0 min, 28 sec Number of successful tactic applications: 619 Number of failed tactic applications: 9382 Results for lemma eqn_sqr: m n : (m ^ 2 == n ^ 2) = (m == n) SUCCESS! Proof Found in EFSM: rewrite -(addn0 n); elim : n 0 => [|n IHn] j; rewrite eqn_exp2r // => /eqP. Tactics applied: 7890 Original Proof: [by rewrite eqn_exp2r.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 20 sec Number of successful tactic applications: 452 Number of failed tactic applications: 7438 Results for lemma mulnS: m n : m * n.+1 = m + m * n SUCCESS! Proof Found in EFSM: by rewrite /maxn addnC; Tactics applied: 279 Original Proof: [by elim: m => // m; rewrite !mulSn !addSn addnCA => ->.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 10 Number of failed tactic applications: 269 Results for lemma addSnnS: m n : m.+1 + n = m + n.+1 SUCCESS! Proof Found in EFSM: rewrite addnS. exact : eqP. Tactics applied: 1493 Original Proof: [by rewrite addnS.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 3 sec Number of successful tactic applications: 45 Number of failed tactic applications: 1448 Results for lemma lt_irrelevance: m n lt_mn1 lt_mn2 : lt_mn1 = lt_mn2 :> (m < n)%coq_nat FAILURE! Tactics applied: 7709 Original Proof: [exact: (@le_irrelevance m.+1).] Proof search time: 0 min, 10 sec Number of successful tactic applications: 135 Number of failed tactic applications: 7574 Results for lemma ltnn: n : n < n = false SUCCESS! Proof Found in EFSM: by elim: n. Tactics applied: 141 Original Proof: [by rewrite ltnNge leqnn.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 7 Number of failed tactic applications: 134 Results for lemma anti_leq: : antisymmetric leq SUCCESS! Proof Found in EFSM: move => n m; by elim: n m => [|n IHn] [|m] //= /IHn->. Tactics applied: 2102 Original Proof: [by move=> m n; rewrite -eqn_leq => /eqP.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 2 sec Number of successful tactic applications: 124 Number of failed tactic applications: 1978 Results for lemma ltn_sub2l: p m n : m < p -> m < n -> p - n < p - m FAILURE! Tactics applied: 10000 Original Proof: [by move/subnSK <-; exact: leq_sub2l.] Proof search time: 0 min, 29 sec Number of successful tactic applications: 711 Number of failed tactic applications: 9290 Results for lemma odd_double: n : odd n.*2 = false SUCCESS! Proof Found in EFSM: by elim: n => //= n ->. Tactics applied: 146 Original Proof: [by rewrite -addnn odd_add addbb.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 7 Number of failed tactic applications: 139 Results for lemma mul1n: : left_id 1 muln FAILURE! Tactics applied: 10000 Original Proof: [exact: addn0.] Proof search time: 0 min, 14 sec Number of successful tactic applications: 401 Number of failed tactic applications: 9600 Results for lemma mulnb: (b1 b2 : bool) : b1 * b2 = b1 && b2 FAILURE! Tactics applied: 9991 Original Proof: [by case: b1; case: b2.] Proof search time: 0 min, 15 sec Number of successful tactic applications: 166 Number of failed tactic applications: 9825 Results for lemma ltn_addr: m n p : m < n -> m < n + p SUCCESS! Proof Found in EFSM: elim : m n => [|m IHm] [|n] //; exact : IHm n. Tactics applied: 681 Original Proof: [by move/leq_trans=> -> //; exact: leq_addr.] Shorter Proof Found? no Proof reused from doubleB proof search time: 0 min, 3 sec Number of successful tactic applications: 46 Number of failed tactic applications: 635 Results for lemma ltn_mul2r: m n1 n2 : (n1 * m < n2 * m) = (0 < m) && (n1 < n2) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite lt0n !ltnNge leq_mul2r negb_or.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 579 Number of failed tactic applications: 9422 Results for lemma mulnSr: m n : m * n.+1 = m * n + m SUCCESS! Proof Found in EFSM: elim : m n => [|m IHm] [|n] //; Tactics applied: 4 Original Proof: [by rewrite addnC mulnS.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 1 Results for lemma eqb0: (b : bool) : (b == 0 :> nat) = ~~ b SUCCESS! Proof Found in EFSM: by case: b. Tactics applied: 101 Original Proof: [by case: b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 98 Results for lemma mul2n: m : 2 * m = m.*2 FAILURE! Tactics applied: 10000 Original Proof: [by rewrite mulSn mul1n addnn.] Proof search time: 0 min, 15 sec Number of successful tactic applications: 320 Number of failed tactic applications: 9681 Results for lemma addn3: m : m + 3 = m.+3 SUCCESS! Proof Found in EFSM: by rewrite addnC. Tactics applied: 286 Original Proof: [by rewrite addnC.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 4 Number of failed tactic applications: 282 Results for lemma addnBA: m n p : p <= n -> m + (n - p) = m + n - p FAILURE! Tactics applied: 10000 Original Proof: [by move=> le_pn; rewrite -{2}(subnK le_pn) addnA addnK.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 483 Number of failed tactic applications: 9518 Results for lemma ltn_addl: m n p : m < n -> m < p + n FAILURE! Tactics applied: 10000 Original Proof: [by move/leq_trans=> -> //; exact: leq_addl.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 621 Number of failed tactic applications: 9380 Results for lemma doubleD: m n : (m + n).*2 = m.*2 + n.*2 FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -!addnn -!addnA (addnCA n).] Proof search time: 0 min, 25 sec Number of successful tactic applications: 530 Number of failed tactic applications: 9471 Results for lemma eq_binP: : Equality.axiom Ndec.Neqb FAILURE! Tactics applied: 10000 Original Proof: [move=> p q; apply: (iffP idP) => [|<-]; last by case: p => //; elim. by case: q; case: p => //; elim=> [p IHp|p IHp|] [q|q|] //=; case/IHp=> ->.] Proof search time: 0 min, 13 sec Number of successful tactic applications: 308 Number of failed tactic applications: 9693 Results for lemma nat_of_succ_gt0: p : Psucc p = p.+1 :> nat FAILURE! Tactics applied: 10000 Original Proof: [by elim: p => //= p ->; rewrite !natTrecE.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 372 Number of failed tactic applications: 9629 Results for lemma sqrn_gt0: n : (0 < n ^ 2) = (0 < n) SUCCESS! Proof Found in EFSM: by case: n. Tactics applied: 117 Original Proof: [exact: (ltn_sqr 0).] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 10 Number of failed tactic applications: 107 Results for lemma eqb1: (b : bool) : (b == 1 :> nat) = b SUCCESS! Proof Found in EFSM: by case: b. Tactics applied: 101 Original Proof: [by case: b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 98 Results for lemma muln0: : right_zero 0 muln SUCCESS! Proof Found in EFSM: rewrite // leq_Sdouble ltnS leq_double. Tactics applied: 67 Original Proof: [by elim.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 15 Number of failed tactic applications: 52 Results for lemma nat_of_binK: : cancel nat_of_bin bin_of_nat FAILURE! Tactics applied: 10000 Original Proof: [case=> //=; elim=> //= p; case: (nat_of_pos p) => //= n [<-]. by rewrite natTrecE !addnS {2}addnn; elim: {1 3}n. by rewrite natTrecE addnS /= addnS {2}addnn; elim: {1 3}n.] Proof search time: 0 min, 15 sec Number of successful tactic applications: 364 Number of failed tactic applications: 9637 Results for lemma nat_of_add_bin: b1 b2 : (b1 + b2)%num = b1 + b2 :> nat SUCCESS! Proof Found in EFSM: case : b1 b2 => [|p] [|q] //=; by rewrite ?(mul1n, nat_of_addn_gt0, mulSn) //= !natTrecE IHp doubleMl. Tactics applied: 1132 Original Proof: [case: b1 b2 => [|p] [|q] //=; exact: nat_of_addn_gt0.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 2 sec Number of successful tactic applications: 39 Number of failed tactic applications: 1093 Results for lemma multE: : mult = muln SUCCESS! Proof Found in EFSM: split ; Tactics applied: 50 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 49 Results for lemma geq_minl: m n : minn m n <= m FAILURE! Tactics applied: 10000 Original Proof: [by rewrite geq_min leqnn.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 555 Number of failed tactic applications: 9446 Results for lemma subSKn: m n : (m.+1 - n).-1 = m - n SUCCESS! Proof Found in EFSM: elim : m n => [|m IHm] [|n] //; exact : IHm n. Tactics applied: 681 Original Proof: [by rewrite -subnS.] Shorter Proof Found? no Proof reused from doubleB proof search time: 0 min, 1 sec Number of successful tactic applications: 17 Number of failed tactic applications: 664 Results for lemma leq_addl: m n : n <= m + n FAILURE! Tactics applied: 10000 Original Proof: [by rewrite addnC leq_addr.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 587 Number of failed tactic applications: 9414 Results for fold 4 Results for lemma leq_exp2l: m n1 n2 : 1 < m -> (m ^ n1 <= m ^ n2) = (n1 <= n2) FAILURE! Tactics applied: 10000 Original Proof: [move=> m_gt1; elim: n1 n2 => [|n1 IHn] [|n2] //; last 1 first. - by rewrite !expnS leq_pmul2l ?IHn // ltnW. - by rewrite expn_gt0 ltnW. by rewrite leqNgt (leq_trans m_gt1) // expnS leq_pmulr // expn_gt0 ltnW.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 633 Number of failed tactic applications: 9368 Results for lemma leq_sub2l: p m n : m <= n -> p - n <= p - m FAILURE! Tactics applied: 10000 Original Proof: [rewrite -(leq_add2r (p - m)) leq_subLR. by apply: leq_trans; rewrite -leq_subLR.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 366 Number of failed tactic applications: 9635 Results for lemma subnn: : self_inverse 0 subn SUCCESS! Proof Found in EFSM: by elim. Tactics applied: 115 Original Proof: [by elim.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 17 Number of failed tactic applications: 98 Results for lemma addnn: n : n + n = n.*2 FAILURE! Tactics applied: 10000 Original Proof: [by apply: eqP; elim: n => // n IHn; rewrite addnS.] Proof search time: 0 min, 26 sec Number of successful tactic applications: 369 Number of failed tactic applications: 9632 Results for lemma ltn_sqr: m n : (m ^ 2 < n ^ 2) = (m < n) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite ltn_exp2r.] Proof search time: 0 min, 28 sec Number of successful tactic applications: 727 Number of failed tactic applications: 9274 Results for lemma addnCA: : left_commutative addn FAILURE! Tactics applied: 10000 Original Proof: [by move=> m n p; elim: m => //= m; rewrite addnS => <-.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 346 Number of failed tactic applications: 9655 Results for lemma mulnE: : muln = muln_rec SUCCESS! Proof Found in EFSM: split ; Tactics applied: 50 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 5 Number of failed tactic applications: 45 Results for lemma maxnA: : associative maxn FAILURE! Tactics applied: 10000 Original Proof: [by move=> m n p; rewrite !(maxnC m) maxnAC.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 525 Number of failed tactic applications: 9476 Results for lemma maxnn: : idempotent maxn FAILURE! Tactics applied: 10000 Original Proof: [by move=> n; apply/maxn_idPl.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 250 Number of failed tactic applications: 9751 Results for lemma addn_minr: : right_distributive addn minn FAILURE! Tactics applied: 10000 Original Proof: [by move=> m1 m2 n; rewrite !minnE subnDl addnBA ?leq_subr.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 276 Number of failed tactic applications: 9725 Results for lemma eq_iter: f f' : f =1 f' -> forall n, iter n f =1 iter n f' FAILURE! Tactics applied: 9102 Original Proof: [by move=> eq_f n x; elim: n => //= n ->; rewrite eq_f.] Proof search time: 0 min, 12 sec Number of successful tactic applications: 119 Number of failed tactic applications: 8983 Results for lemma leq_pmul2r: m n1 n2 : 0 < m -> (n1 * m <= n2 * m) = (n1 <= n2) FAILURE! Tactics applied: 10000 Original Proof: [by move/prednK <-; rewrite leq_mul2r.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 1128 Number of failed tactic applications: 8873 Results for lemma maxn_idPr: {m n} : reflect (maxn m n = n) (m <= n) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite maxnC; apply: maxn_idPl.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 446 Number of failed tactic applications: 9555 Results for lemma nat_Cauchy: m n : 2 * (m * n) <= m ^ 2 + n ^ 2 ?= iff (m == n) FAILURE! Tactics applied: 10000 Original Proof: [wlog le_nm: m n / n <= m. by case: (leqP m n); auto; rewrite eq_sym addnC (mulnC m); auto. apply/leqifP; case: ifP => [/eqP-> | ne_mn]; first by rewrite mulnn addnn mul2n. by rewrite -subn_gt0 -sqrn_sub // sqrn_gt0 subn_gt0 ltn_neqAle eq_sym ne_mn.] Proof search time: 0 min, 38 sec Number of successful tactic applications: 342 Number of failed tactic applications: 9659 Results for lemma odd_opp: i m : odd m = false -> i < m -> odd (m - i) = odd i FAILURE! Tactics applied: 10000 Original Proof: [by move=> oddm lt_im; rewrite (odd_sub (ltnW lt_im)) oddm.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 341 Number of failed tactic applications: 9660 Results for lemma expn_gt0: m n : (0 < m ^ n) = (0 < m) || (n == 0) FAILURE! Tactics applied: 10000 Original Proof: [by case: m => [|m]; elim: n => //= n IHn; rewrite expnS // addn_gt0 IHn.] Proof search time: 0 min, 29 sec Number of successful tactic applications: 2056 Number of failed tactic applications: 7945 Results for lemma min0n: : left_zero 0 minn SUCCESS! Proof Found in EFSM: by case. Tactics applied: 79 Original Proof: [by case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 17 Number of failed tactic applications: 62 Results for lemma minnK: m n : maxn (minn m n) m = m FAILURE! Tactics applied: 10000 Original Proof: [exact/maxn_idPr/geq_minl.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 178 Number of failed tactic applications: 9823 Results for lemma maxnACA: : interchange maxn maxn FAILURE! Tactics applied: 10000 Original Proof: [by move=> m n p q; rewrite -!maxnA (maxnCA n).] Proof search time: 0 min, 24 sec Number of successful tactic applications: 340 Number of failed tactic applications: 9661 Results for lemma fact_gt0: n : n`! > 0 FAILURE! Tactics applied: 10000 Original Proof: [by elim: n => //= n IHn; rewrite muln_gt0.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 952 Number of failed tactic applications: 9049 Results for lemma eqnE: : eqn = eq_op SUCCESS! Proof Found in EFSM: split ; Tactics applied: 50 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 5 Number of failed tactic applications: 45 Results for lemma eqnP: : Equality.axiom eqn FAILURE! Tactics applied: 10000 Original Proof: [move=> n m; apply: (iffP idP) => [|<-]; last by elim n. by elim: n m => [|n IHn] [|m] //= /IHn->.] Proof search time: 0 min, 14 sec Number of successful tactic applications: 280 Number of failed tactic applications: 9721 Results for lemma addn_gt0: m n : (0 < m + n) = (0 < m) || (0 < n) SUCCESS! Proof Found in EFSM: elim : m n => [|m IHm] [|n] //; Tactics applied: 4 Original Proof: [by rewrite !lt0n -negb_and addn_eq0.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 1 Results for lemma leq_ltn_trans: n m p : m <= n -> n < p -> m < p SUCCESS! Proof Found in EFSM: move => e_gt0; by apply: leq_trans; Tactics applied: 1226 Original Proof: [move=> Hmn; exact: leq_trans.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 4 sec Number of successful tactic applications: 105 Number of failed tactic applications: 1121 Results for lemma ltn_double: m n : (m.*2 < n.*2) = (m < n) SUCCESS! Proof Found in EFSM: elim : m n => [|m IHm] [|n] //; exact : IHm n. Tactics applied: 663 Original Proof: [by rewrite 2!ltnNge leq_double.] Shorter Proof Found? no Proof reused from doubleB This proof contained a loop around a state proof search time: 0 min, 2 sec Number of successful tactic applications: 30 Number of failed tactic applications: 633 Results for lemma ltn_trans: n m p : m < n -> n < p -> m < p FAILURE! Tactics applied: 10000 Original Proof: [by move=> lt_mn /ltnW; exact: leq_trans.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 637 Number of failed tactic applications: 9364 Results for lemma subSn: m n : m <= n -> n.+1 - m = (n - m).+1 SUCCESS! Proof Found in EFSM: elim : m n => [|m IHm] [|n] //; exact : IHm n. Tactics applied: 663 Original Proof: [by rewrite -add1n => /addnBA <-.] Shorter Proof Found? no Proof reused from doubleB This proof contained a loop around a state proof search time: 0 min, 2 sec Number of successful tactic applications: 52 Number of failed tactic applications: 611 Results for lemma ltn_pexp2l: m n1 n2 : 0 < m -> m ^ n1 < m ^ n2 -> n1 < n2 FAILURE! Tactics applied: 10000 Original Proof: [by case: m => [|[|m]] // _; [rewrite !exp1n | rewrite ltn_exp2l].] Proof search time: 0 min, 19 sec Number of successful tactic applications: 724 Number of failed tactic applications: 9277 Results for lemma leq_sub: m1 m2 n1 n2 : m1 <= m2 -> n2 <= n1 -> m1 - n1 <= m2 - n2 FAILURE! Tactics applied: 10000 Original Proof: [by move/(leq_sub2r n1)=> le_m12 /(leq_sub2l m2); apply: leq_trans.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 577 Number of failed tactic applications: 9424 Results for lemma double0: : 0.*2 = 0 SUCCESS! Proof Found in EFSM: split ; Tactics applied: 50 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 5 Number of failed tactic applications: 45 Results for lemma subn_gt0: m n : (0 < n - m) = (m < n) SUCCESS! Proof Found in EFSM: elim : m n => [|m IHm] [|n] //; exact : IHm n. Tactics applied: 663 Original Proof: [by elim: m n => [|m IHm] [|n] //; exact: IHm n.] Shorter Proof Found? no Proof reused from doubleB This proof contained a loop around a state proof search time: 0 min, 2 sec Number of successful tactic applications: 28 Number of failed tactic applications: 635 Results for lemma lt0n_neq0: n : 0 < n -> n != 0 SUCCESS! Proof Found in EFSM: by case: n. Tactics applied: 100 Original Proof: [by case: n.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 17 Number of failed tactic applications: 83 Results for lemma factE: : factorial = fact_rec SUCCESS! Proof Found in EFSM: split ; Tactics applied: 50 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 5 Number of failed tactic applications: 45 Results for lemma minnSS: m n : minn m.+1 n.+1 = (minn m n).+1 FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -(addn_minr 1).] Proof search time: 0 min, 29 sec Number of successful tactic applications: 356 Number of failed tactic applications: 9645 Results for lemma maxn_minl: : left_distributive maxn minn FAILURE! Tactics applied: 10000 Original Proof: [move=> m1 m2 n; wlog le_m21: m1 m2 / m2 <= m1. move=> IH; case/orP: (leq_total m2 m1) => /IH //. by rewrite minnC [in R in _ = R]minnC. rewrite (minn_idPr le_m21); apply/esym/minn_idPr. by rewrite geq_max leq_maxr leq_max le_m21.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 688 Number of failed tactic applications: 9313 Results for fold 5 Results for lemma maxn_minr: : right_distributive maxn minn FAILURE! Tactics applied: 10000 Original Proof: [by move=> m n1 n2; rewrite !(maxnC m) maxn_minl.] Proof search time: 0 min, 32 sec Number of successful tactic applications: 2654 Number of failed tactic applications: 7347 Results for lemma leqif_refl: m C : reflect (m <= m ?= iff C) C SUCCESS! Proof Found in EFSM: apply : (iffP idP); last 1 first. case => //=; elim => //= p; by elim: p => //= p <-. by elim: m. Tactics applied: 3175 Original Proof: [by apply: (iffP idP) => [-> | <-] //; split; rewrite ?eqxx.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 7 sec Number of successful tactic applications: 494 Number of failed tactic applications: 2681 Results for lemma geq_max: m n1 n2 : (m >= maxn n1 n2) = (m >= n1) && (m >= n2) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -ltnS gtn_max.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 726 Number of failed tactic applications: 9275 Results for lemma leq_max: m n1 n2 : (m <= maxn n1 n2) = (m <= n1) || (m <= n2) FAILURE! Tactics applied: 10000 Original Proof: [without loss le_n21: n1 n2 / n2 <= n1. by case/orP: (leq_total n2 n1) => le_n12; last rewrite maxnC orbC; apply. by rewrite (maxn_idPl le_n21) orb_idr // => /leq_trans->.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 1223 Number of failed tactic applications: 8778 Results for lemma leq_pmulr: m n : n > 0 -> m <= m * n FAILURE! Tactics applied: 10000 Original Proof: [by move/leq_pmull; rewrite mulnC.] Proof search time: 0 min, 26 sec Number of successful tactic applications: 1465 Number of failed tactic applications: 8536 Results for lemma subnKC: m n : m <= n -> m + (n - m) = n FAILURE! Tactics applied: 10000 Original Proof: [by elim: m n => [|m IHm] [|n] // /(IHm n) {2}<-.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 1101 Number of failed tactic applications: 8900 Results for lemma eqn_exp2r: m n e : e > 0 -> (m ^ e == n ^ e) = (m == n) FAILURE! Tactics applied: 10000 Original Proof: [by move=> e_gt0; rewrite !eqn_leq !leq_exp2r.] Proof search time: 0 min, 34 sec Number of successful tactic applications: 783 Number of failed tactic applications: 9218 Results for lemma minusE: : minus = subn SUCCESS! Proof Found in EFSM: split ; Tactics applied: 1 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 1 Number of failed tactic applications: 0 Results for lemma iter_muln_1: m n : iter n (muln m) 1 = m ^ n FAILURE! Tactics applied: 10000 Original Proof: [by rewrite iter_muln muln1.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 1460 Number of failed tactic applications: 8541 Results for lemma subnE: : subn = subn_rec SUCCESS! Proof Found in EFSM: split ; Tactics applied: 1 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 1 Number of failed tactic applications: 0 Results for lemma half_bit_double: n (b : bool) : (b + n.*2)./2 = n FAILURE! Tactics applied: 10000 Original Proof: [by case: b; rewrite /= (half_double, uphalf_double).] Proof search time: 0 min, 18 sec Number of successful tactic applications: 1903 Number of failed tactic applications: 8098 Results for lemma iteropS: idx n op x : iterop n.+1 op x idx = iter n (op x) x SUCCESS! Proof Found in EFSM: by elim: n => //= n ->. Tactics applied: 125 Original Proof: [by elim: n => //= n ->.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 5 Number of failed tactic applications: 120 Results for lemma expnE: : expn = expn_rec SUCCESS! Proof Found in EFSM: split ; Tactics applied: 1 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 1 Number of failed tactic applications: 0 Results for lemma mulnA: : associative muln FAILURE! Tactics applied: 10000 Original Proof: [by move=> m n p; elim: m => //= m; rewrite mulSn mulnDl => ->.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 610 Number of failed tactic applications: 9391 Results for lemma addn_negb: (b : bool) : ~~ b + b = 1 SUCCESS! Proof Found in EFSM: by case: b. Tactics applied: 79 Original Proof: [by case: b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 1 Number of failed tactic applications: 78 Results for lemma eq_ex_maxn: (P Q : pred nat) m n exP ubP exQ ubQ : P =1 Q -> @ex_maxn P m exP ubP = @ex_maxn Q n exQ ubQ FAILURE! Tactics applied: 10000 Original Proof: [move=> eqPQ; case: ex_maxnP => i Pi max_i; case: ex_maxnP => j Pj max_j. by apply/eqP; rewrite eqn_leq max_i ?eqPQ // max_j -?eqPQ.] Proof search time: 0 min, 27 sec Number of successful tactic applications: 1872 Number of failed tactic applications: 8129 Results for lemma iter_succn: m n : iter n succn m = m + n SUCCESS! Proof Found in EFSM: by elim: n => //= n ->. Tactics applied: 125 Original Proof: [by elim: n => //= n ->.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 8 Number of failed tactic applications: 117 Results for lemma addn_eq0: m n : (m + n == 0) = (m == 0) && (n == 0) SUCCESS! Proof Found in EFSM: elim : m n => [|m IHm] [|n] //; Tactics applied: 44 Original Proof: [by case: m; case: n.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 4 Number of failed tactic applications: 40 Results for lemma sqrnD: m n : (m + n) ^ 2 = m ^ 2 + n ^ 2 + 2 * (m * n) FAILURE! Tactics applied: 10000 Original Proof: [rewrite -!mulnn mul2n mulnDr !mulnDl (mulnC n) -!addnA. by congr (_ + _); rewrite addnA addnn addnC.] Proof search time: 0 min, 30 sec Number of successful tactic applications: 531 Number of failed tactic applications: 9470 Results for lemma lt0b: (b : bool) : (b > 0) = b SUCCESS! Proof Found in EFSM: by case: b. Tactics applied: 79 Original Proof: [by case: b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 1 Number of failed tactic applications: 78 Results for lemma half_gt0: n : (0 < n./2) = (1 < n) SUCCESS! Proof Found in EFSM: by case: n => [|[|[]]]. Tactics applied: 97 Original Proof: [by case: n => [|[]].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 5 Number of failed tactic applications: 92 Results for lemma posnP: n : eqn0_xor_gt0 n (n == 0) (0 < n) SUCCESS! Proof Found in EFSM: elim : n => [|n IHn]; constructor ; rewrite // ltnNge le_mn. Tactics applied: 1519 Original Proof: [by case: n; constructor.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 2 sec Number of successful tactic applications: 60 Number of failed tactic applications: 1459 Results for lemma ltP: m n : reflect (m < n)%coq_nat (m < n) FAILURE! Tactics applied: 10000 Original Proof: [exact leP.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 517 Number of failed tactic applications: 9484 Results for lemma nat_of_addn_gt0: p q : (p + q)%positive = p + q :> nat FAILURE! Tactics applied: 10000 Original Proof: [apply: fst (Pplus_carry p q = (p + q).+1 :> nat) _. elim: p q => [p IHp|p IHp|] [q|q|] //=; rewrite !natTrecE //; by rewrite ?IHp ?nat_of_succ_gt0 ?(doubleS, doubleD, addn1, addnS).] Proof search time: 0 min, 20 sec Number of successful tactic applications: 2777 Number of failed tactic applications: 7224 Results for lemma leqNgt: m n : (m <= n) = ~~ (n < m) SUCCESS! Proof Found in EFSM: elim : m n => [|m IHm] [|n] //; exact : IHm n. Tactics applied: 729 Original Proof: [by elim: m n => [|m IHm] [|n] //; exact: IHm n.] Shorter Proof Found? no Proof reused from doubleB proof search time: 0 min, 2 sec Number of successful tactic applications: 35 Number of failed tactic applications: 694 Results for lemma add_mulE: n m s : add_mul n m s = addn (muln n m) s FAILURE! Tactics applied: 10000 Original Proof: [by elim: n => //= n IHn in m s *; rewrite IHn addE addnCA addnA.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 1773 Number of failed tactic applications: 8228 Results for lemma leq_mul: m1 m2 n1 n2 : m1 <= n1 -> m2 <= n2 -> m1 * m2 <= n1 * n2 FAILURE! Tactics applied: 10000 Original Proof: [move=> le_mn1 le_mn2; apply (@leq_trans (m1 * n2)). by rewrite leq_mul2l le_mn2 orbT. by rewrite leq_mul2r le_mn1 orbT.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 577 Number of failed tactic applications: 9424 Results for lemma odd_geq: m n : odd n -> (m <= n) = (m./2.*2 <= n) FAILURE! Tactics applied: 10000 Original Proof: [move=> odd_n; rewrite -{1}[m]odd_double_half -[n]odd_double_half odd_n. by case: (odd m); rewrite // leq_Sdouble ltnS leq_double.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 1096 Number of failed tactic applications: 8905 Results for lemma nat_irrelevance: (x y : nat) (E E' : x = y) : E = E' FAILURE! Tactics applied: 10000 Original Proof: [exact: eq_irrelevance.] Proof search time: 0 min, 16 sec Number of successful tactic applications: 3367 Number of failed tactic applications: 6634 Results for lemma leqSpred: n : n <= n.-1.+1 SUCCESS! Proof Found in EFSM: by case: n. Tactics applied: 95 Original Proof: [by case: n => /=.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 5 Number of failed tactic applications: 90 Results for lemma ltn_sub2r: p m n : p < n -> m < n -> m - p < n - p FAILURE! Tactics applied: 10000 Original Proof: [by move/subnSK <-; exact: (@leq_sub2r p.+1).] Proof search time: 0 min, 26 sec Number of successful tactic applications: 1145 Number of failed tactic applications: 8856 Results for lemma iterSr: n f x : iter n.+1 f x = iter n f (f x) SUCCESS! Proof Found in EFSM: by elim: n => //= n ->. Tactics applied: 125 Original Proof: [by elim: n => //= n <-.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 5 Number of failed tactic applications: 120 Results for lemma half_leq: m n : m <= n -> m./2 <= n./2 FAILURE! Tactics applied: 10000 Original Proof: [by move/subnK <-; rewrite halfD addnA leq_addl.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 1343 Number of failed tactic applications: 8658 Results for lemma ltn_exp2r: m n e : e > 0 -> (m ^ e < n ^ e) = (m < n) FAILURE! Tactics applied: 10000 Original Proof: [move=> e_gt0; apply/idP/idP=> [|ltmn]. rewrite !ltnNge; apply: contra => lemn. by elim: e {e_gt0} => // e IHe; rewrite !expnS leq_mul. by elim: e e_gt0 => // [[|e] IHe] _; rewrite ?expn1 // ltn_mul // IHe.] Proof search time: 0 min, 32 sec Number of successful tactic applications: 766 Number of failed tactic applications: 9235 Results for lemma ltn_leqif: a b C : a <= b ?= iff C -> (a < b) = ~~ C FAILURE! Tactics applied: 10000 Original Proof: [by move=> le_ab; rewrite ltnNge (geq_leqif le_ab).] Proof search time: 0 min, 23 sec Number of successful tactic applications: 640 Number of failed tactic applications: 9361 Results for fold 6 Results for lemma iteriS: n f x : iteri n.+1 f x = f n (iteri n f x) SUCCESS! Proof Found in EFSM: auto. Tactics applied: 52 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 49 Results for lemma maxnE: m n : maxn m n = m + (n - m) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite /maxn addnC; case: leqP => [/eqnP-> | /ltnW/subnK].] Proof search time: 0 min, 23 sec Number of successful tactic applications: 1606 Number of failed tactic applications: 8395 Results for lemma leq_b1: (b : bool) : b <= 1 SUCCESS! Proof Found in EFSM: by case: b. Tactics applied: 98 Original Proof: [by case: b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 95 Results for lemma addn1: n : n + 1 = n.+1 SUCCESS! Proof Found in EFSM: exact : addnC. Tactics applied: 75 Original Proof: [by rewrite addnC.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 5 Number of failed tactic applications: 70 Results for lemma maxn0: : right_id 0 maxn SUCCESS! Proof Found in EFSM: case => //=; Tactics applied: 41 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 13 Number of failed tactic applications: 28 Results for lemma iter_add: n m f x : iter (n + m) f x = iter n f (iter m f x) SUCCESS! Proof Found in EFSM: by elim: n => //= n ->. Tactics applied: 143 Original Proof: [by elim: n => //= n ->.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 8 Number of failed tactic applications: 135 Results for lemma muln1: : right_id 1 muln FAILURE! Tactics applied: 10000 Original Proof: [by move=> n; rewrite mulnSr muln0.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 1409 Number of failed tactic applications: 8592 Results for lemma maxKn: m n : minn n (maxn m n) = n FAILURE! Tactics applied: 10000 Original Proof: [exact/minn_idPl/leq_maxr.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 1981 Number of failed tactic applications: 8020 Results for lemma minn_maxr: : right_distributive minn maxn FAILURE! Tactics applied: 10000 Original Proof: [by move=> m n1 n2; rewrite !(minnC m) minn_maxl.] Proof search time: 0 min, 28 sec Number of successful tactic applications: 2858 Number of failed tactic applications: 7143 Results for lemma addKn: n : cancel (addn n) (subn^~ n) SUCCESS! Proof Found in EFSM: case => //=; rewrite -(addn0 n); by elim: n. Tactics applied: 1357 Original Proof: [by move=> m; rewrite /= -{2}[n]addn0 subnDl subn0.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 2 sec Number of successful tactic applications: 73 Number of failed tactic applications: 1284 Results for lemma oddb: (b : bool) : odd b = b SUCCESS! Proof Found in EFSM: by case: b. Tactics applied: 98 Original Proof: [by case: b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 95 Results for lemma addn_maxl: : left_distributive addn maxn FAILURE! Tactics applied: 10000 Original Proof: [by move=> m1 m2 n; rewrite !maxnE subnDr addnAC.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 1484 Number of failed tactic applications: 8517 Results for lemma mulnbl: (b : bool) n : b * n = (if b then n else 0) FAILURE! Tactics applied: 10000 Original Proof: [by case: b; rewrite ?mul1n.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 3076 Number of failed tactic applications: 6925 Results for lemma iter_predn: m n : iter n predn m = m - n FAILURE! Tactics applied: 10000 Original Proof: [by elim: n m => /= [|n IHn] m; rewrite ?subn0 // IHn subnS.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 2305 Number of failed tactic applications: 7696 Results for lemma maxnC: : commutative maxn FAILURE! Tactics applied: 10000 Original Proof: [by move=> m n; rewrite /maxn; case ltngtP.] Proof search time: 0 min, 16 sec Number of successful tactic applications: 1744 Number of failed tactic applications: 8257 Results for lemma mulE: : mul =2 muln FAILURE! Tactics applied: 10000 Original Proof: [by case=> //= n m; rewrite add_mulE addnC.] Proof search time: 0 min, 16 sec Number of successful tactic applications: 1575 Number of failed tactic applications: 8426 Results for lemma maxnCA: : left_commutative maxn FAILURE! Tactics applied: 10000 Original Proof: [by move=> m n p; rewrite !maxnA (maxnC m).] Proof search time: 0 min, 20 sec Number of successful tactic applications: 1522 Number of failed tactic applications: 8479 Results for lemma expnMn: m1 m2 n : (m1 * m2) ^ n = m1 ^ n * m2 ^ n FAILURE! Tactics applied: 10000 Original Proof: [by elim: n => // n IHn; rewrite !expnS IHn -!mulnA (mulnCA m2).] Proof search time: 0 min, 22 sec Number of successful tactic applications: 3314 Number of failed tactic applications: 6687 Results for lemma expn0: m : m ^ 0 = 1 SUCCESS! Proof Found in EFSM: auto. Tactics applied: 52 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 51 Results for lemma ltngtP: m n : compare_nat m n (m < n) (n < m) (m == n) FAILURE! Tactics applied: 10000 Original Proof: [rewrite ltn_neqAle eqn_leq; case: ltnP; first by constructor. by rewrite leq_eqVlt orbC; case: leqP; constructor; first exact/eqnP.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 200 Number of failed tactic applications: 9801 Results for lemma ltn_subRL: m n p : (n < p - m) = (m + n < p) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite !ltnNge leq_subLR.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 1741 Number of failed tactic applications: 8260 Results for lemma add2n: m : 2 + m = m.+2 SUCCESS! Proof Found in EFSM: auto. Tactics applied: 52 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 51 Results for lemma leq_add2l: p m n : (p + m <= p + n) = (m <= n) SUCCESS! Proof Found in EFSM: by elim: p. Tactics applied: 160 Original Proof: [by elim: p.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 8 Number of failed tactic applications: 152 Results for lemma subn_eq0: m n : (m - n == 0) = (m <= n) SUCCESS! Proof Found in EFSM: elim : m n => [|m IHm] [|n] //; Tactics applied: 45 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 2 Number of failed tactic applications: 43 Results for lemma neq_ltn: m n : (m != n) = (m < n) || (n < m) SUCCESS! Proof Found in EFSM: elim : m n => [|m IHm] [|n] //; exact : IHm n. Tactics applied: 353 Original Proof: [by rewrite eqn_leq negb_and orbC -!ltnNge.] Shorter Proof Found? no Proof reused from doubleB proof search time: 0 min, 1 sec Number of successful tactic applications: 11 Number of failed tactic applications: 342 Results for lemma sqrn_sub: m n : n <= m -> (m - n) ^ 2 = m ^ 2 + n ^ 2 - 2 * (m * n) FAILURE! Tactics applied: 10000 Original Proof: [move/subnK=> def_m; rewrite -{2}def_m sqrnD -addnA addnAC. by rewrite -2!addnA addnn -mul2n -mulnDr -mulnDl def_m addnK.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 823 Number of failed tactic applications: 9178 Results for lemma iterS: n f x : iter n.+1 f x = f (iter n f x) SUCCESS! Proof Found in EFSM: auto. Tactics applied: 52 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 49 Results for lemma odd_add: m n : odd (m + n) = odd m (+) odd n FAILURE! Tactics applied: 10000 Original Proof: [by elim: m => [|m IHn] //=; rewrite -addTb IHn addbA addTb.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 1730 Number of failed tactic applications: 8271 Results for lemma addnC: : commutative addn SUCCESS! Proof Found in EFSM: move => n m; elim : n => //= n; auto ; rewrite addnS. by elim. Tactics applied: 7193 Original Proof: [by move=> m n; rewrite -{1}[n]addn0 addnCA addn0.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 12 sec Number of successful tactic applications: 1396 Number of failed tactic applications: 5797 Results for lemma subn_sqr: m n : m ^ 2 - n ^ 2 = (m - n) * (m + n) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite mulnBl !mulnDr addnC (mulnC m) subnDl !mulnn.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 1946 Number of failed tactic applications: 8055 Results for lemma addn_min_max: m n : minn m n + maxn m n = m + n FAILURE! Tactics applied: 10000 Original Proof: [by rewrite /minn /maxn; case: ltngtP => // [_|->] //; exact: addnC.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 1621 Number of failed tactic applications: 8380 Results for lemma leq_addr: m n : n <= n + m SUCCESS! Proof Found in EFSM: by elim: n. Tactics applied: 138 Original Proof: [by rewrite -{1}[n]addn0 leq_add2l.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 8 Number of failed tactic applications: 130 Results for lemma leq_pred: n : n.-1 <= n SUCCESS! Proof Found in EFSM: by case: n. Tactics applied: 114 Original Proof: [by case: n => /=.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 5 Number of failed tactic applications: 109 Results for lemma oddE: : odd =1 oddn FAILURE! Tactics applied: 10000 Original Proof: [move=> n; rewrite -{1}[n]odd_double_half addnC. by elim: n./2 => //=; case (oddn n).] Proof search time: 0 min, 18 sec Number of successful tactic applications: 1468 Number of failed tactic applications: 8533 Results for lemma muln_eq1: m n : (m * n == 1) = (m == 1) && (n == 1) FAILURE! Tactics applied: 10000 Original Proof: [by case: m n => [|[|m]] [|[|n]] //; rewrite muln0.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 1782 Number of failed tactic applications: 8219 Results for fold 7 Results for lemma addn4: m : m + 4 = m.+4 SUCCESS! Proof Found in EFSM: by rewrite addnC. Tactics applied: 244 Original Proof: [by rewrite addnC.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 241 Results for lemma subnAC: : right_commutative subn FAILURE! Tactics applied: 10000 Original Proof: [by move=> m n p; rewrite -!subnDA addnC.] Proof search time: 0 min, 16 sec Number of successful tactic applications: 260 Number of failed tactic applications: 9741 Results for lemma nat_semi_morph: : semi_morph 0 1 addn muln (@eq _) 0%num 1%num Nplus Nmult pred1 nat_of_bin FAILURE! Tactics applied: 10000 Original Proof: [by move: nat_of_add_bin nat_of_mul_bin; split=> //= m n; move/eqP->.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 1231 Number of failed tactic applications: 8770 Results for lemma add4n: m : 4 + m = m.+4 SUCCESS! Proof Found in EFSM: split ; Tactics applied: 40 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 37 Results for lemma minKn: m n : maxn n (minn m n) = n FAILURE! Tactics applied: 10000 Original Proof: [exact/maxn_idPl/geq_minr.] Proof search time: 0 min, 26 sec Number of successful tactic applications: 2780 Number of failed tactic applications: 7221 Results for lemma minnA: : associative minn FAILURE! Tactics applied: 10000 Original Proof: [by move=> m n p; rewrite minnC minnAC (minnC n).] Proof search time: 0 min, 21 sec Number of successful tactic applications: 418 Number of failed tactic applications: 9583 Results for lemma maxn_mull: : left_distributive muln maxn FAILURE! Tactics applied: 10000 Original Proof: [by move=> m1 m2 n; rewrite -!(mulnC n) maxn_mulr.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 653 Number of failed tactic applications: 9348 Results for lemma addIn: : left_injective addn FAILURE! Tactics applied: 10000 Original Proof: [move=> p m n; rewrite -!(addnC p); apply addnI.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 427 Number of failed tactic applications: 9574 Results for lemma succnK: : cancel succn predn SUCCESS! Proof Found in EFSM: split ; Tactics applied: 40 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 17 Number of failed tactic applications: 23 Results for lemma exp1n: n : 1 ^ n = 1 FAILURE! Tactics applied: 351 Original Proof: [by elim: n => // n; rewrite expnS mul1n.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 4 Number of failed tactic applications: 347 Results for lemma factS: n : (n.+1)`! = n.+1 * n`! SUCCESS! Proof Found in EFSM: split ; Tactics applied: 40 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 5 Number of failed tactic applications: 35 Results for lemma halfD: m n : (m + n)./2 = (odd m && odd n) + (m./2 + n./2) FAILURE! Tactics applied: 10000 Original Proof: [rewrite -{1}[n]odd_double_half addnCA -{1}[m]odd_double_half -addnA -doubleD. by do 2!case: odd; rewrite /= ?add0n ?half_double ?uphalf_double.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 410 Number of failed tactic applications: 9591 Results for lemma doubleB: m n : (m - n).*2 = m.*2 - n.*2 SUCCESS! Proof Found in EFSM: elim : m n => [|m IHm] [|n] //; exact : IHm n. Tactics applied: 642 Original Proof: [elim: m n => [|m IHm] [|n] //; exact: IHm n.] Shorter Proof Found? no Proof reused from leq_eqVlt proof search time: 0 min, 1 sec Number of successful tactic applications: 13 Number of failed tactic applications: 629 Results for lemma ex_maxnP: : ex_maxn_spec ex_maxn FAILURE! Tactics applied: 10000 Original Proof: [rewrite /ex_maxn; case: ex_minnP => i Pmi min_i; split=> // j Pj. have le_i_mj: i <= m - j by rewrite min_i // subKn // ubP. rewrite -subn_eq0 subnBA ?(leq_trans le_i_mj) ?leq_subr //. by rewrite addnC -subnBA ?ubP.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 521 Number of failed tactic applications: 9480 Results for lemma leq_min: m n1 n2 : (m <= minn n1 n2) = (m <= n1) && (m <= n2) FAILURE! Tactics applied: 10000 Original Proof: [wlog le_n21: n1 n2 / n2 <= n1. by case/orP: (leq_total n2 n1) => ?; last rewrite minnC andbC; auto. by rewrite /minn ltnNge le_n21 /= andbC; case: leqP => // /leq_trans->.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 472 Number of failed tactic applications: 9529 Results for lemma mul_expE: m n p : mul_exp m n p = muln (expn m n) p FAILURE! Tactics applied: 10000 Original Proof: [by elim: n => [|n IHn] in p *; rewrite ?mul1n //= expnS IHn mulE mulnCA mulnA.] Proof search time: 0 min, 30 sec Number of successful tactic applications: 603 Number of failed tactic applications: 9398 Results for lemma leq_mul2r: m n1 n2 : (n1 * m <= n2 * m) = (m == 0) || (n1 <= n2) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -!(mulnC m) leq_mul2l.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 2835 Number of failed tactic applications: 7166 Results for lemma mul0n: : left_zero 0 muln SUCCESS! Proof Found in EFSM: split ; Tactics applied: 40 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 17 Number of failed tactic applications: 23 Results for lemma addnI: : right_injective addn FAILURE! Tactics applied: 10000 Original Proof: [by move=> p m n Heq; apply: eqP; rewrite -(eqn_add2l p) Heq eqxx.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 427 Number of failed tactic applications: 9574 Results for lemma find_ex_minn: : {m | P m & forall n, P n -> n >= m} FAILURE! Tactics applied: 343 Original Proof: [have: forall n, P n -> n >= 0 by []. have: acc_nat 0. case exP => n; rewrite -(addn0 n); elim: n 0 => [|n IHn] j; first by left. rewrite addSnnS; right; exact: IHn. move: 0; fix 2 => m IHm m_lb; case Pm: (P m); first by exists m. apply: find_ex_minn m.+1 _ _ => [|n Pn]; first by case: IHm; rewrite ?Pm. by rewrite ltn_neqAle m_lb //; case: eqP Pm => // -> /idP[].] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 343 Results for lemma mulnAC: : right_commutative muln FAILURE! Tactics applied: 10000 Original Proof: [by move=> m n p; rewrite -!mulnA (mulnC n).] Proof search time: 0 min, 19 sec Number of successful tactic applications: 291 Number of failed tactic applications: 9710 Results for lemma ltnNge: m n : (m < n) = ~~ (n <= m) SUCCESS! Proof Found in EFSM: elim : m n => [|m IHm] [|n] //; exact : IHm n. Tactics applied: 625 Original Proof: [by rewrite leqNgt.] Shorter Proof Found? no Proof reused from leq_eqVlt proof search time: 0 min, 1 sec Number of successful tactic applications: 13 Number of failed tactic applications: 612 Results for lemma mulnCA: : left_commutative muln FAILURE! Tactics applied: 10000 Original Proof: [by move=> m n1 n2; rewrite !mulnA (mulnC m).] Proof search time: 0 min, 20 sec Number of successful tactic applications: 641 Number of failed tactic applications: 9360 Results for lemma mulSnr: m n : m.+1 * n = m * n + n SUCCESS! Proof Found in EFSM: by rewrite /maxn addnC; Tactics applied: 235 Original Proof: [exact: addnC.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 8 Number of failed tactic applications: 227 Results for lemma subnK: m n : m <= n -> (n - m) + m = n SUCCESS! Proof Found in EFSM: by elim: m n => [|m IHm] [|n] // /(IHm n) {2}<-. Tactics applied: 99 Original Proof: [by rewrite addnC; exact: subnKC.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 20 Number of failed tactic applications: 79 Results for lemma sqrn_inj: : injective (expn ^~ 2) FAILURE! Tactics applied: 10000 Original Proof: [exact: expIn.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 328 Number of failed tactic applications: 9673 Results for lemma maxnSS: m n : maxn m.+1 n.+1 = (maxn m n).+1 FAILURE! Tactics applied: 10000 Original Proof: [by rewrite !maxnE.] Proof search time: 0 min, 29 sec Number of successful tactic applications: 3270 Number of failed tactic applications: 6731 Results for lemma ex_minnP: : ex_minn_spec ex_minn FAILURE! Tactics applied: 10000 Original Proof: [by rewrite /ex_minn; case: find_ex_minn.] Proof search time: 0 min, 15 sec Number of successful tactic applications: 437 Number of failed tactic applications: 9564 Results for lemma fact0: : 0`! = 1 SUCCESS! Proof Found in EFSM: split ; Tactics applied: 40 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 37 Results for lemma mulnn: m : m * m = m ^ 2 SUCCESS! Proof Found in EFSM: split ; Tactics applied: 40 Original Proof: [by rewrite !expnS muln1.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 37 Results for lemma doubleMr: m n : (m * n).*2 = m * n.*2 FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -!muln2 mulnA.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 425 Number of failed tactic applications: 9576 Results for lemma expnI: m : 1 < m -> injective (expn m) FAILURE! Tactics applied: 10000 Original Proof: [by move=> m_gt1 e1 e2 /eqP; rewrite eqn_exp2l // => /eqP.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 504 Number of failed tactic applications: 9497 Results for lemma expnSr: m n : m ^ n.+1 = m ^ n * m FAILURE! Tactics applied: 10000 Original Proof: [by rewrite mulnC expnS.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 605 Number of failed tactic applications: 9396 Results for lemma minnAC: : right_commutative minn FAILURE! Tactics applied: 10000 Original Proof: [by move=> m n p; rewrite !minnE -subnDA subnAC -maxnE maxnC maxnE subnAC subnDA.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 338 Number of failed tactic applications: 9663 Results for lemma ltn_pmul2l: m n1 n2 : 0 < m -> (m * n1 < m * n2) = (n1 < n2) FAILURE! Tactics applied: 10000 Original Proof: [by move/prednK <-; rewrite ltn_mul2l.] Proof search time: 0 min, 26 sec Number of successful tactic applications: 611 Number of failed tactic applications: 9390 Results for fold 8 Results for lemma odd_exp: m n : odd (m ^ n) = (n == 0) || odd m FAILURE! Tactics applied: 10000 Original Proof: [by elim: n => // n IHn; rewrite expnS odd_mul {}IHn orbC; case odd.] Proof search time: 0 min, 26 sec Number of successful tactic applications: 1013 Number of failed tactic applications: 8988 Results for lemma prednK: n : 0 < n -> n.-1.+1 = n SUCCESS! Proof Found in EFSM: by case: n. Tactics applied: 139 Original Proof: [exact: ltn_predK.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 17 Number of failed tactic applications: 122 Results for lemma addnA: : associative addn FAILURE! Tactics applied: 10000 Original Proof: [by move=> m n p; rewrite (addnC n) addnCA addnC.] Proof search time: 0 min, 15 sec Number of successful tactic applications: 750 Number of failed tactic applications: 9251 Results for lemma ltnS: m n : (m < n.+1) = (m <= n) SUCCESS! Proof Found in EFSM: elim : m n => [|m IHm] [|n] //; Tactics applied: 6 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 2 Number of failed tactic applications: 4 Results for lemma iter_succn_0: n : iter n succn 0 = n SUCCESS! Proof Found in EFSM: by elim: n => //= n ->. Tactics applied: 167 Original Proof: [exact: iter_succn.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 164 Results for lemma doubleMl: m n : (m * n).*2 = m.*2 * n FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -!mul2n mulnA.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 745 Number of failed tactic applications: 9256 Results for lemma maxn_idPl: {m n} : reflect (maxn m n = m) (m >= n) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -subn_eq0 -(eqn_add2l m) addn0 -maxnE; apply: eqP.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 808 Number of failed tactic applications: 9193 Results for lemma addnS: m n : m + n.+1 = (m + n).+1 SUCCESS! Proof Found in EFSM: elim : m n => [|m IHm] [|n] //; Tactics applied: 6 Original Proof: [by elim: m.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 2 Number of failed tactic applications: 4 Results for lemma doubleK: : cancel double half SUCCESS! Proof Found in EFSM: have sub2nn n : n.*2 - n = n by rewrite -addnn addKn. case => //= n; by elim: n => //= n ->. Tactics applied: 2153 Original Proof: [by elim=> //= n ->.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 4 sec Number of successful tactic applications: 93 Number of failed tactic applications: 2060 Results for lemma subn1: n : n - 1 = n.-1 SUCCESS! Proof Found in EFSM: by case: n => [|[|[]]]. Tactics applied: 141 Original Proof: [by case: n => [|[]].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 138 Results for lemma leqif_add: m1 n1 C1 m2 n2 C2 : m1 <= n1 ?= iff C1 -> m2 <= n2 ?= iff C2 -> m1 + m2 <= n1 + n2 ?= iff C1 && C2 FAILURE! Tactics applied: 10000 Original Proof: [rewrite -(mono_leqif (leq_add2r m2)) -(mono_leqif (leq_add2l n1) m2). exact: leqif_trans.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 631 Number of failed tactic applications: 9370 Results for lemma leqW: m n : m <= n -> m <= n.+1 SUCCESS! Proof Found in EFSM: by move/leq_trans=> -> //; Tactics applied: 192 Original Proof: [by move=> le_mn; exact: ltnW.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 20 Number of failed tactic applications: 172 Results for lemma odd_mul: m n : odd (m * n) = odd m && odd n FAILURE! Tactics applied: 10000 Original Proof: [by elim: m => //= m IHm; rewrite odd_add -addTb andb_addl -IHm.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 749 Number of failed tactic applications: 9252 Results for lemma leq_trans: n m p : m <= n -> n <= p -> m <= p FAILURE! Tactics applied: 10000 Original Proof: [by elim: n m p => [|i IHn] [|m] [|p] //; exact: IHn m p.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 784 Number of failed tactic applications: 9217 Results for lemma minn_mull: : left_distributive muln minn FAILURE! Tactics applied: 10000 Original Proof: [by move=> m1 m2 n; rewrite -!(mulnC n) minn_mulr.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 495 Number of failed tactic applications: 9506 Results for lemma muln_gt0: m n : (0 < m * n) = (0 < m) && (0 < n) SUCCESS! Proof Found in EFSM: elim : m n => [|m IHm] [|n] //; first by rewrite !muln0. Tactics applied: 689 Original Proof: [by case: m n => // m [|n] //=; rewrite muln0.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 1 sec Number of successful tactic applications: 34 Number of failed tactic applications: 655 Results for lemma subnBA: m n p : p <= n -> m - (n - p) = m + p - n FAILURE! Tactics applied: 10000 Original Proof: [by move=> le_pn; rewrite -{2}(subnK le_pn) subnDr.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 746 Number of failed tactic applications: 9255 Results for lemma ltn_mul2l: m n1 n2 : (m * n1 < m * n2) = (0 < m) && (n1 < n2) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite lt0n !ltnNge leq_mul2l negb_or.] Proof search time: 0 min, 26 sec Number of successful tactic applications: 756 Number of failed tactic applications: 9245 Results for lemma neq0_lt0n: n : (n == 0) = false -> 0 < n SUCCESS! Proof Found in EFSM: by case: n. Tactics applied: 139 Original Proof: [by case: n.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 17 Number of failed tactic applications: 122 Results for lemma subKn: m n : m <= n -> n - (n - m) = m FAILURE! Tactics applied: 10000 Original Proof: [by move/subnBA->; rewrite addKn.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 841 Number of failed tactic applications: 9160 Results for lemma add0n: : left_id 0 addn SUCCESS! Proof Found in EFSM: constructor ; Tactics applied: 50 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 17 Number of failed tactic applications: 33 Results for lemma add3n: m : 3 + m = m.+3 SUCCESS! Proof Found in EFSM: constructor ; Tactics applied: 50 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 49 Results for lemma iter_muln: m n p : iter n (muln m) p = m ^ n * p FAILURE! Tactics applied: 10000 Original Proof: [by elim: n => /= [|n ->]; rewrite ?mul1n // expnS mulnA.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 731 Number of failed tactic applications: 9270 Results for lemma odd_gt2: n : odd n -> n > 1 -> n > 2 SUCCESS! Proof Found in EFSM: by case: n => [|[|[]]]. Tactics applied: 141 Original Proof: [by move=> odd_n n_gt1; rewrite odd_geq.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 31 Number of failed tactic applications: 110 Results for lemma expnD: m n1 n2 : m ^ (n1 + n2) = m ^ n1 * m ^ n2 FAILURE! Tactics applied: 10000 Original Proof: [by elim: n1 => [|n1 IHn]; rewrite !(mul1n, expnS) // IHn mulnA.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 565 Number of failed tactic applications: 9436 Results for lemma minnn: : idempotent minn FAILURE! Tactics applied: 10000 Original Proof: [by move=> n; apply/minn_idPl.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 512 Number of failed tactic applications: 9489 Results for lemma nat_power_theory: : power_theory 1 muln (@eq _) nat_of_bin expn FAILURE! Tactics applied: 10000 Original Proof: [split; exact: nat_of_exp_bin.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 486 Number of failed tactic applications: 9515 Results for lemma nat_AGM2: m n : 4 * (m * n) <= (m + n) ^ 2 ?= iff (m == n) FAILURE! Tactics applied: 10000 Original Proof: [rewrite -[4]/(2 * 2) -mulnA mul2n -addnn sqrnD; apply/leqifP. by rewrite ltn_add2r eqn_add2r ltn_neqAle !nat_Cauchy; case: ifP => ->.] Proof search time: 0 min, 27 sec Number of successful tactic applications: 660 Number of failed tactic applications: 9341 Results for lemma mulnDl: : left_distributive muln addn FAILURE! Tactics applied: 10000 Original Proof: [by move=> m1 m2 n; elim: m1 => //= m1 IHm; rewrite -addnA -IHm.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 715 Number of failed tactic applications: 9286 Results for lemma muln2: m : m * 2 = m.*2 FAILURE! Tactics applied: 10000 Original Proof: [by rewrite mulnC mul2n.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 560 Number of failed tactic applications: 9441 Results for lemma leqif_geq: m n : m <= n -> m <= n ?= iff (m >= n) SUCCESS! Proof Found in EFSM: elim : m n => [|m IHm] [|n] //; exact : IHm n. Tactics applied: 677 Original Proof: [by move=> lemn; split=> //; rewrite eqn_leq lemn.] Shorter Proof Found? yes Proof reused from leq_eqVlt proof search time: 0 min, 2 sec Number of successful tactic applications: 60 Number of failed tactic applications: 617 Results for lemma plusE: : plus = addn SUCCESS! Proof Found in EFSM: constructor ; Tactics applied: 50 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 49 Results for lemma succn_inj: : injective succn SUCCESS! Proof Found in EFSM: move => n m; elim : n => [|n IHn]; case => //= n; Tactics applied: 2264 Original Proof: [by move=> n m [].] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 3 sec Number of successful tactic applications: 112 Number of failed tactic applications: 2152 Results for lemma addnE: : addn = addn_rec SUCCESS! Proof Found in EFSM: constructor ; Tactics applied: 50 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 49 Results for lemma ltn_eqF: m n : m < n -> m == n = false SUCCESS! Proof Found in EFSM: elim : m n => [|m IHm] [|n] //; exact : IHm n. Tactics applied: 677 Original Proof: [by move/gtn_eqF; rewrite eq_sym.] Shorter Proof Found? no Proof reused from leq_eqVlt proof search time: 0 min, 1 sec Number of successful tactic applications: 52 Number of failed tactic applications: 625 Results for fold 9 Results for lemma expE: : exp =2 expn FAILURE! Tactics applied: 10000 Original Proof: [by move=> m [|n] //=; rewrite mul_expE expnS mulnC.] Proof search time: 0 min, 15 sec Number of successful tactic applications: 394 Number of failed tactic applications: 9607 Results for lemma leq_Sdouble: m n : (m.*2 <= n.*2.+1) = (m <= n) SUCCESS! Proof Found in EFSM: elim : m n => [|m IHm] [|n] //; exact : IHm n. Tactics applied: 512 Original Proof: [by rewrite leqNgt ltn_Sdouble -leqNgt.] Shorter Proof Found? no Proof reused from leq_eqVlt proof search time: 0 min, 1 sec Number of successful tactic applications: 16 Number of failed tactic applications: 496 Results for lemma ltnP: m n : ltn_xor_geq m n (n <= m) (m < n) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -(ltnS n); case: leqP; constructor.] Proof search time: 0 min, 14 sec Number of successful tactic applications: 365 Number of failed tactic applications: 9636 Results for lemma leqnSn: n : n <= n.+1 SUCCESS! Proof Found in EFSM: by elim: n => // n IHn; Tactics applied: 169 Original Proof: [by elim: n.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 7 Number of failed tactic applications: 162 Results for lemma mulnACA: : interchange muln muln FAILURE! Tactics applied: 10000 Original Proof: [by move=> m n p q; rewrite -!mulnA (mulnCA n).] Proof search time: 0 min, 24 sec Number of successful tactic applications: 850 Number of failed tactic applications: 9151 Results for lemma mulnBl: : left_distributive muln subn FAILURE! Tactics applied: 10000 Original Proof: [move=> m n [|p]; first by rewrite !muln0. by elim: m n => // [m IHm] [|n] //; rewrite mulSn subnDl -IHm.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 689 Number of failed tactic applications: 9312 Results for lemma minn0: : right_zero 0 minn SUCCESS! Proof Found in EFSM: case => //=; Tactics applied: 63 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 15 Number of failed tactic applications: 48 Results for lemma sub0n: : left_zero 0 subn SUCCESS! Proof Found in EFSM: case => //=; Tactics applied: 63 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 15 Number of failed tactic applications: 48 Results for lemma minn_mulr: : right_distributive muln minn FAILURE! Tactics applied: 10000 Original Proof: [by case=> // m n1 n2; rewrite /minn (fun_if (muln _)) ltn_pmul2l.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 687 Number of failed tactic applications: 9314 Results for lemma eqn0Ngt: n : (n == 0) = ~~ (n > 0) SUCCESS! Proof Found in EFSM: by case: n. Tactics applied: 141 Original Proof: [by case: n.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 7 Number of failed tactic applications: 134 Results for lemma muln_eq0: m n : (m * n == 0) = (m == 0) || (n == 0) SUCCESS! Proof Found in EFSM: elim : m n => [|m IHm] [|n] //; rewrite (muln0, mulnS) // mulSn => ->. Tactics applied: 517 Original Proof: [by case: m n => // m [|n] //=; rewrite muln0.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 1 sec Number of successful tactic applications: 15 Number of failed tactic applications: 502 Results for lemma eqSS: m n : (m.+1 == n.+1) = (m == n) SUCCESS! Proof Found in EFSM: auto. Tactics applied: 67 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 4 Number of failed tactic applications: 63 Results for lemma mulnBr: : right_distributive muln subn FAILURE! Tactics applied: 10000 Original Proof: [by move=> m n p; rewrite !(mulnC m) mulnBl.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 692 Number of failed tactic applications: 9309 Results for lemma leq_add: m1 m2 n1 n2 : m1 <= n1 -> m2 <= n2 -> m1 + m2 <= n1 + n2 FAILURE! Tactics applied: 10000 Original Proof: [by move=> le_mn1 le_mn2; rewrite (@leq_trans (m1 + n2)) ?leq_add2l ?leq_add2r.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 443 Number of failed tactic applications: 9558 Results for lemma eqn_add2r: p m n : (m + p == n + p) = (m == n) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -!(addnC p) eqn_add2l.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 3194 Number of failed tactic applications: 6807 Results for lemma odd_gt0: n : odd n -> n > 0 SUCCESS! Proof Found in EFSM: by case: n. Tactics applied: 141 Original Proof: [by case: n.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 24 Number of failed tactic applications: 117 Results for lemma gtn_eqF: m n : m < n -> n == m = false SUCCESS! Proof Found in EFSM: elim : m n => [|m IHm] [|n] //; exact : IHm n. Tactics applied: 1331 Original Proof: [by rewrite eqn_leq (leqNgt n) => ->.] Shorter Proof Found? no Proof reused from leq_eqVlt proof search time: 0 min, 2 sec Number of successful tactic applications: 76 Number of failed tactic applications: 1255 Results for lemma iter_addn: m n p : iter n (addn m) p = m * n + p FAILURE! Tactics applied: 10000 Original Proof: [by elim: n => /= [|n ->]; rewrite ?muln0 // mulnS addnA.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 2416 Number of failed tactic applications: 7585 Results for lemma bin_of_natK: : cancel bin_of_nat nat_of_bin FAILURE! Tactics applied: 10000 Original Proof: [have sub2nn n : n.*2 - n = n by rewrite -addnn addKn. case=> //= n; rewrite -{3}[n]sub2nn. by elim: n {2 4}n => // m IHm [|[|n]] //=; rewrite IHm // natTrecE sub2nn.] Proof search time: 0 min, 14 sec Number of successful tactic applications: 392 Number of failed tactic applications: 9609 Results for lemma gtn_max: m n1 n2 : (m > maxn n1 n2) = (m > n1) && (m > n2) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite !ltnNge leq_max negb_or.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 592 Number of failed tactic applications: 9409 Results for lemma max0n: : left_id 0 maxn SUCCESS! Proof Found in EFSM: case => //=; Tactics applied: 63 Original Proof: [by case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 15 Number of failed tactic applications: 48 Results for lemma nat_of_exp_bin: n (b : N) : n ^ b = pow_N 1 muln n b FAILURE! Tactics applied: 10000 Original Proof: [case: b => [|p] /=; first exact: expn0. by elim: p => //= p <-; rewrite natTrecE mulnn -expnM muln2 ?expnS.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 2695 Number of failed tactic applications: 7306 Results for lemma leq_subLR: m n p : (m - n <= p) = (m <= n + p) SUCCESS! Proof Found in EFSM: elim : m n => [|m IHm] [|n] //; exact : IHm n. Tactics applied: 478 Original Proof: [by rewrite -subn_eq0 -subnDA.] Shorter Proof Found? no Proof reused from leq_eqVlt proof search time: 0 min, 1 sec Number of successful tactic applications: 14 Number of failed tactic applications: 464 Results for lemma leq0n: n : 0 <= n SUCCESS! Proof Found in EFSM: auto. Tactics applied: 67 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 64 Results for lemma minn_idPl: {m n} : reflect (minn m n = m) (m <= n) FAILURE! Tactics applied: 10000 Original Proof: [rewrite (sameP maxn_idPr eqP) -(eqn_add2l m) eq_sym -addn_min_max eqn_add2r. exact: eqP.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 3253 Number of failed tactic applications: 6748 Results for lemma leq_pexp2l: m n1 n2 : 0 < m -> n1 <= n2 -> m ^ n1 <= m ^ n2 FAILURE! Tactics applied: 10000 Original Proof: [by case: m => [|[|m]] // _; [rewrite !exp1n | rewrite leq_exp2l].] Proof search time: 0 min, 29 sec Number of successful tactic applications: 668 Number of failed tactic applications: 9333 Results for lemma eqn_exp2l: m n1 n2 : 1 < m -> (m ^ n1 == m ^ n2) = (n1 == n2) FAILURE! Tactics applied: 10000 Original Proof: [by move=> m_gt1; rewrite !eqn_leq !leq_exp2l.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 401 Number of failed tactic applications: 9600 Results for lemma subnDA: m n p : n - (m + p) = (n - m) - p SUCCESS! Proof Found in EFSM: elim : m n => [|m IHm] [|n] //; exact : IHm n. Tactics applied: 478 Original Proof: [by elim: m n => [|m IHm] [|n]; try exact (IHm n).] Shorter Proof Found? no Proof reused from leq_eqVlt proof search time: 0 min, 1 sec Number of successful tactic applications: 14 Number of failed tactic applications: 464 Results for lemma subn0: : right_id 0 subn SUCCESS! Proof Found in EFSM: case => //=; Tactics applied: 63 Original Proof: [by case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 15 Number of failed tactic applications: 48 Results for lemma leq_add2r: p m n : (m + p <= n + p) = (m <= n) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -!(addnC p); exact: leq_add2l.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 3251 Number of failed tactic applications: 6750 Results for lemma addn_minl: : left_distributive addn minn FAILURE! Tactics applied: 10000 Original Proof: [by move=> m1 m2 n; rewrite -!(addnC n) addn_minr.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 620 Number of failed tactic applications: 9381 Results for lemma leq_double: m n : (m.*2 <= n.*2) = (m <= n) SUCCESS! Proof Found in EFSM: elim : m n => [|m IHm] [|n] //; exact : IHm n. Tactics applied: 512 Original Proof: [by rewrite /leq -doubleB; case (m - n).] Shorter Proof Found? no Proof reused from leq_eqVlt proof search time: 0 min, 1 sec Number of successful tactic applications: 16 Number of failed tactic applications: 496 Results for lemma leqnn: n : n <= n SUCCESS! Proof Found in EFSM: by elim: n => // n IHn; Tactics applied: 169 Original Proof: [by elim: n.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 7 Number of failed tactic applications: 162 Results for lemma leq_sub2r: p m n : m <= n -> m - p <= n - p FAILURE! Tactics applied: 10000 Original Proof: [by move=> le_mn; rewrite leq_subLR (leq_trans le_mn) // -leq_subLR.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 374 Number of failed tactic applications: 9627 Results for lemma subSnn: n : n.+1 - n = 1 SUCCESS! Proof Found in EFSM: by elim: n => // n IHn; Tactics applied: 169 Original Proof: [exact (addnK n 1).] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 7 Number of failed tactic applications: 162 Results for fold 10 Results for lemma ltn_Sdouble: m n : (m.*2.+1 < n.*2) = (m < n) SUCCESS! Proof Found in EFSM: elim : m n => [|m IHm] [|n] //; exact : IHm n. Tactics applied: 704 Original Proof: [by rewrite -doubleS leq_double.] Shorter Proof Found? no Proof reused from leq_eqVlt proof search time: 0 min, 2 sec Number of successful tactic applications: 24 Number of failed tactic applications: 680 Results for lemma minn_idPr: {m n} : reflect (minn m n = n) (m >= n) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite minnC; apply: minn_idPl.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 1615 Number of failed tactic applications: 8386 Results for lemma expnAC: m n1 n2 : (m ^ n1) ^ n2 = (m ^ n2) ^ n1 FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -!expnM mulnC.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 972 Number of failed tactic applications: 9029 Results for lemma gtn_min: m n1 n2 : (m > minn n1 n2) = (m > n1) || (m > n2) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite !ltnNge leq_min negb_and.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 753 Number of failed tactic applications: 9248 Results for lemma subnDr: p m n : (m + p) - (n + p) = m - n FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -!(addnC p) subnDl.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 1539 Number of failed tactic applications: 8462 Results for lemma sub1b: (b : bool) : 1 - b = ~~ b SUCCESS! Proof Found in EFSM: by case: b. Tactics applied: 69 Original Proof: [by case: b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 68 Results for lemma leq_pmul2l: m n1 n2 : 0 < m -> (m * n1 <= m * n2) = (n1 <= n2) FAILURE! Tactics applied: 10000 Original Proof: [by move/prednK=> <-; rewrite leq_mul2l.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 764 Number of failed tactic applications: 9237 Results for lemma minnE: m n : minn m n = m - (m - n) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -(subnDl n) -maxnE -addn_min_max addnK minnC.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 610 Number of failed tactic applications: 9391 Results for lemma expn1: m : m ^ 1 = m SUCCESS! Proof Found in EFSM: constructor ; Tactics applied: 39 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 38 Results for lemma minnACA: : interchange minn minn FAILURE! Tactics applied: 10000 Original Proof: [by move=> m n p q; rewrite -!minnA (minnCA n).] Proof search time: 0 min, 25 sec Number of successful tactic applications: 548 Number of failed tactic applications: 9453 Results for lemma leqn0: n : (n <= 0) = (n == 0) SUCCESS! Proof Found in EFSM: by case: n. Tactics applied: 85 Original Proof: [by case: n.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 82 Results for lemma expnS: m n : m ^ n.+1 = m * m ^ n FAILURE! Tactics applied: 10000 Original Proof: [by case: n; rewrite ?muln1.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 752 Number of failed tactic applications: 9249 Results for lemma add1n: n : 1 + n = n.+1 SUCCESS! Proof Found in EFSM: constructor ; Tactics applied: 39 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 36 Results for lemma eqn_mul2r: m n1 n2 : (n1 * m == n2 * m) = (m == 0) || (n1 == n2) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite eqn_leq !leq_mul2r -orb_andr -eqn_leq.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 527 Number of failed tactic applications: 9474 Results for lemma ltn_predK: m n : m < n -> n.-1.+1 = n SUCCESS! Proof Found in EFSM: elim : m n => [|m IHm] [|n] //; Tactics applied: 41 Original Proof: [by case: n.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 15 Number of failed tactic applications: 26 Results for lemma nat_semi_ring: : semi_ring_theory 0 1 addn muln (@eq _) FAILURE! Tactics applied: 10000 Original Proof: [exact: mk_srt add0n addnC addnA mul1n mul0n mulnC mulnA mulnDl.] Proof search time: 0 min, 37 sec Number of successful tactic applications: 1918 Number of failed tactic applications: 8083 Results for lemma leqif_eq: m n : m <= n -> m <= n ?= iff (m == n) SUCCESS! Proof Found in EFSM: elim : m n => [|m IHm] [|n] //; Tactics applied: 41 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 19 Number of failed tactic applications: 22 Results for lemma subn_if_gt: T m n F (E : T) : (if m.+1 - n is m'.+1 then F m' else E) = (if n <= m then F (m - n) else E) SUCCESS! Proof Found in EFSM: elim : m n => [|m IHm] [|n] //; rewrite IHm // natTrecE sub2nn. Tactics applied: 680 Original Proof: [by case: leqP => [le_nm | /eqnP-> //]; rewrite -{1}(subnK le_nm) -addSn addnK.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 2 sec Number of successful tactic applications: 14 Number of failed tactic applications: 666 Results for lemma expIn: e : e > 0 -> injective (expn^~ e) FAILURE! Tactics applied: 10000 Original Proof: [by move=> e_gt1 m n /eqP; rewrite eqn_exp2r // => /eqP.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 544 Number of failed tactic applications: 9457 Results for lemma odd_ltn: m n : odd n -> (n < m) = (n < m./2.*2) FAILURE! Tactics applied: 10000 Original Proof: [by move=> odd_n; rewrite !ltnNge odd_geq.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 737 Number of failed tactic applications: 9264 Results for lemma ltn_neqAle: m n : (m < n) = (m != n) && (m <= n) SUCCESS! Proof Found in EFSM: elim : m n => [|m IHm] [|n] //; exact : IHm n. Tactics applied: 696 Original Proof: [by rewrite ltnNge leq_eqVlt negb_or -leqNgt eq_sym.] Shorter Proof Found? no Proof reused from leq_eqVlt proof search time: 0 min, 2 sec Number of successful tactic applications: 14 Number of failed tactic applications: 682 Results for lemma maxn_mulr: : right_distributive muln maxn FAILURE! Tactics applied: 10000 Original Proof: [by case=> // m n1 n2; rewrite /maxn (fun_if (muln _)) ltn_pmul2l.] Proof search time: 0 min, 31 sec Number of successful tactic applications: 441 Number of failed tactic applications: 9560 Results for lemma ltn_Pmull: m n : 1 < n -> 0 < m -> m < n * m FAILURE! Tactics applied: 10000 Original Proof: [by move=> lt1n m_gt0; rewrite -{1}[m]mul1n ltn_pmul2r.] Proof search time: 0 min, 27 sec Number of successful tactic applications: 818 Number of failed tactic applications: 9183 Results for lemma geq_leqif: a b C : a <= b ?= iff C -> (b <= a) = C FAILURE! Tactics applied: 10000 Original Proof: [by case=> le_ab; rewrite eqn_leq le_ab.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 870 Number of failed tactic applications: 9131 Results for lemma addn0: : right_id 0 addn SUCCESS! Proof Found in EFSM: case => //=; Tactics applied: 53 Original Proof: [by move=> n; apply/eqP; elim: n.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 15 Number of failed tactic applications: 38 Results for lemma eqn_pmul2l: m n1 n2 : 0 < m -> (m * n1 == m * n2) = (n1 == n2) FAILURE! Tactics applied: 10000 Original Proof: [by move/prednK <-; rewrite eqn_mul2l.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 775 Number of failed tactic applications: 9226 OVERALL RESULTS SUMMARY EFSMProver proved 135 out of 341 lemmas. Success rate of 39.589442815249264% There were 0 errors. 205 proof attempts exhausted the automaton On average, a proof was found after applying 409 tactics The longest proof consisted of 6 tactics There were 9 shorter proofs found Of the 205 failures, 194 of them used all 10000 tactics There were 121 reused proofs found There were 14 novel proofs found Of the 205 failures, the average number of tactics used was 9613 On average, a proof was found after 0 min, 1 sec On average, a failed proof attempt took 0 min, 21 sec On average, any (success or failure) proof attempt took 0 min, 13 sec The longest time to find a proof was 0 min, 20 sec The shortest time to find a proof was 0 min, 0 sec There were 0 proofs containing repeated tactics There were 3 proofs that repeated states