Results for fold 1 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, 22 sec Number of successful tactic applications: 527 Number of failed tactic applications: 9474 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] //; try exact (IHm n). Tactics applied: 311 Original Proof: [by rewrite -add1n => /addnBA <-.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 1 sec Number of successful tactic applications: 18 Number of failed tactic applications: 293 Results for lemma leq_sqr: m n : (m ^ 2 <= n ^ 2) = (m <= n) SUCCESS! Proof Found in EFSM: elim : m n => [|m IHm] [|n] //; rewrite leqNgt ltn_exp2r // -leqNgt. split => //; Tactics applied: 1859 Original Proof: [by rewrite leq_exp2r.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 6 sec Number of successful tactic applications: 153 Number of failed tactic applications: 1706 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] //; try exact (IHm n). Tactics applied: 311 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, 1 sec Number of successful tactic applications: 6 Number of failed tactic applications: 305 Results for lemma ltnSn: n : n < n.+1 SUCCESS! Proof Found in EFSM: auto. Tactics applied: 54 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: 53 Results for lemma eqn0Ngt: n : (n == 0) = ~~ (n > 0) 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, 1 sec Number of successful tactic applications: 3 Number of failed tactic applications: 111 Results for lemma posnP: n : eqn0_xor_gt0 n (n == 0) (0 < n) FAILURE! Tactics applied: 10000 Original Proof: [by case: n; constructor.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 405 Number of failed tactic applications: 9596 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, 16 sec Number of successful tactic applications: 510 Number of failed tactic applications: 9491 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, 1 sec Number of successful tactic applications: 3 Number of failed tactic applications: 111 Results for lemma prednK: n : 0 < n -> n.-1.+1 = n SUCCESS! Proof Found in EFSM: by case: n. Tactics applied: 114 Original Proof: [exact: ltn_predK.] 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: 99 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: 545 Number of failed tactic applications: 9456 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: 903 Number of failed tactic applications: 9098 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, 16 sec Number of successful tactic applications: 521 Number of failed tactic applications: 9480 Results for lemma ltn_addr: m n p : m < n -> m < n + p SUCCESS! Proof Found in EFSM: elim : m n => [|m IHm] [|n] //; try exact (IHm n). Tactics applied: 311 Original Proof: [by move/leq_trans=> -> //; exact: leq_addr.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 1 sec Number of successful tactic applications: 22 Number of failed tactic applications: 289 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, 22 sec Number of successful tactic applications: 620 Number of failed tactic applications: 9381 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: 511 Number of failed tactic applications: 9490 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, 15 sec Number of successful tactic applications: 686 Number of failed tactic applications: 9315 Results for lemma iteriS: n f x : iteri n.+1 f x = f n (iteri n f x) SUCCESS! Proof Found in EFSM: constructor ; Tactics applied: 9 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: 8 Results for lemma add3n: m : 3 + m = m.+3 SUCCESS! Proof Found in EFSM: constructor ; Tactics applied: 9 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: 8 Results for lemma max0n: : left_id 0 maxn SUCCESS! Proof Found in EFSM: case => //=; Tactics applied: 62 Original Proof: [by case.] 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: 47 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, 22 sec Number of successful tactic applications: 431 Number of failed tactic applications: 9570 Results for lemma expn0: m : m ^ 0 = 1 SUCCESS! Proof Found in EFSM: constructor ; Tactics applied: 9 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: 8 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, 17 sec Number of successful tactic applications: 643 Number of failed tactic applications: 9358 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, 14 sec Number of successful tactic applications: 515 Number of failed tactic applications: 9486 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, 22 sec Number of successful tactic applications: 697 Number of failed tactic applications: 9304 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, 18 sec Number of successful tactic applications: 601 Number of failed tactic applications: 9400 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, 16 sec Number of successful tactic applications: 517 Number of failed tactic applications: 9484 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, 26 sec Number of successful tactic applications: 448 Number of failed tactic applications: 9553 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, 13 sec Number of successful tactic applications: 208 Number of failed tactic applications: 9793 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: 1339 Number of failed tactic applications: 8662 Results for lemma ltn0Sn: n : 0 < n.+1 SUCCESS! Proof Found in EFSM: constructor ; Tactics applied: 9 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: 8 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, 16 sec Number of successful tactic applications: 422 Number of failed tactic applications: 9579 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, 22 sec Number of successful tactic applications: 1367 Number of failed tactic applications: 8634 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, 21 sec Number of successful tactic applications: 506 Number of failed tactic applications: 9495 Results for lemma oddb: (b : bool) : odd b = b SUCCESS! Proof Found in EFSM: by case: b. Tactics applied: 100 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: 3 Number of failed tactic applications: 97 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, 24 sec Number of successful tactic applications: 886 Number of failed tactic applications: 9115 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, 25 sec Number of successful tactic applications: 931 Number of failed tactic applications: 9070 Results for lemma mulnS: m n : m * n.+1 = m + m * n SUCCESS! Proof Found in EFSM: by rewrite /maxn addnC; Tactics applied: 271 Original Proof: [by elim: m => // m; rewrite !mulSn !addSn addnCA => ->.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 6 Number of failed tactic applications: 265 Results for lemma addn4: m : m + 4 = m.+4 SUCCESS! Proof Found in EFSM: exact : addnC. Tactics applied: 17 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: 16 Results for lemma ltnn: n : n < n = false SUCCESS! Proof Found in EFSM: by elim: n. Tactics applied: 136 Original Proof: [by rewrite ltnNge leqnn.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 3 Number of failed tactic applications: 133 Results for lemma mulSnr: m n : m.+1 * n = m * n + n SUCCESS! Proof Found in EFSM: exact : addnC. Tactics applied: 17 Original Proof: [exact: addnC.] 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: 13 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, 16 sec Number of successful tactic applications: 648 Number of failed tactic applications: 9353 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: 408 Number of failed tactic applications: 9593 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, 26 sec Number of successful tactic applications: 3194 Number of failed tactic applications: 6807 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, 26 sec Number of successful tactic applications: 1191 Number of failed tactic applications: 8810 Results for lemma leq_b1: (b : bool) : b <= 1 SUCCESS! Proof Found in EFSM: by case: b. Tactics applied: 100 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: 3 Number of failed tactic applications: 97 Results for lemma sub0n: : left_zero 0 subn SUCCESS! Proof Found in EFSM: constructor ; Tactics applied: 9 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: 8 Results for lemma multE: : mult = muln SUCCESS! Proof Found in EFSM: constructor ; Tactics applied: 9 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: 8 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, 16 sec Number of successful tactic applications: 517 Number of failed tactic applications: 9484 Results for lemma exp0n: n : 0 < n -> 0 ^ n = 0 SUCCESS! Proof Found in EFSM: by case: n => [|[|[]]]. Tactics applied: 116 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: 19 Number of failed tactic applications: 97 Results for lemma anti_leq: : antisymmetric leq FAILURE! Tactics applied: 10000 Original Proof: [by move=> m n; rewrite -eqn_leq => /eqP.] Proof search time: 0 min, 14 sec Number of successful tactic applications: 517 Number of failed tactic applications: 9484 Results for lemma mulnE: : muln = muln_rec SUCCESS! Proof Found in EFSM: constructor ; Tactics applied: 9 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: 8 Results for lemma sqrn_gt0: n : (0 < n ^ 2) = (0 < n) SUCCESS! Proof Found in EFSM: by case: n. Tactics applied: 114 Original Proof: [exact: (ltn_sqr 0).] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 7 Number of failed tactic applications: 107 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, 22 sec Number of successful tactic applications: 620 Number of failed tactic applications: 9381 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, 22 sec Number of successful tactic applications: 701 Number of failed tactic applications: 9300 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, 22 sec Number of successful tactic applications: 700 Number of failed tactic applications: 9301 Results for lemma doubleE: : double = double_rec SUCCESS! Proof Found in EFSM: constructor ; Tactics applied: 9 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: 8 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, 1 sec Number of successful tactic applications: 2 Number of failed tactic applications: 2 Results for lemma mulnn: m : m * m = m ^ 2 SUCCESS! Proof Found in EFSM: constructor ; Tactics applied: 9 Original Proof: [by rewrite !expnS muln1.] 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: 8 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, 17 sec Number of successful tactic applications: 531 Number of failed tactic applications: 9470 Results for lemma subSnn: n : n.+1 - n = 1 SUCCESS! Proof Found in EFSM: by elim: n. Tactics applied: 136 Original Proof: [exact (addnK n 1).] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 3 Number of failed tactic applications: 133 Results for lemma leq_total: m n : (m <= n) || (m >= n) SUCCESS! Proof Found in EFSM: elim : m n => [|m IHm] [|n] //; try exact (IHm n). Tactics applied: 307 Original Proof: [by rewrite -implyNb -ltnNge; apply/implyP; exact: ltnW.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 1 sec Number of successful tactic applications: 6 Number of failed tactic applications: 301 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: 419 Number of failed tactic applications: 9582 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: 4 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: 2 Number of failed tactic applications: 2 Results for lemma factE: : factorial = fact_rec SUCCESS! Proof Found in EFSM: constructor ; Tactics applied: 9 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: 8 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, 28 sec Number of successful tactic applications: 1289 Number of failed tactic applications: 8712 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, 23 sec Number of successful tactic applications: 332 Number of failed tactic applications: 9669 Results for lemma neq_ltn: m n : (m != n) = (m < n) || (n < m) SUCCESS! Proof Found in EFSM: elim : m n => [|m IHm] [|n] //; try exact (IHm n). Tactics applied: 311 Original Proof: [by rewrite eqn_leq negb_and orbC -!ltnNge.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 1 sec Number of successful tactic applications: 6 Number of failed tactic applications: 305 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, 18 sec Number of successful tactic applications: 768 Number of failed tactic applications: 9233 Results for fold 2 Results for lemma ltnS: m n : (m < n.+1) = (m <= n) SUCCESS! Proof Found in EFSM: split ; Tactics applied: 33 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: 30 Results for lemma leqW: m n : m <= n -> m <= n.+1 SUCCESS! Proof Found in EFSM: by move/leq_trans=> -> //; Tactics applied: 129 Original Proof: [by move=> le_mn; exact: ltnW.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 14 Number of failed tactic applications: 115 Results for lemma maxn0: : right_id 0 maxn SUCCESS! Proof Found in EFSM: split ; Tactics applied: 33 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 11 Number of failed tactic applications: 22 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, 18 sec Number of successful tactic applications: 1320 Number of failed tactic applications: 8681 Results for lemma mulnb: (b1 b2 : bool) : b1 * b2 = b1 && b2 FAILURE! Tactics applied: 318 Original Proof: [by case: b1; case: b2.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 318 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: 618 Original Proof: [by elim: m n => [|m IHm] [|n]; try exact (IHm n).] Shorter Proof Found? no Proof reused from eqn_leq proof search time: 0 min, 1 sec Number of successful tactic applications: 10 Number of failed tactic applications: 608 Results for lemma lt0n_neq0: n : 0 < n -> n != 0 SUCCESS! Proof Found in EFSM: by case: n. Tactics applied: 76 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: 12 Number of failed tactic applications: 64 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, 29 sec Number of successful tactic applications: 1493 Number of failed tactic applications: 8508 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, 23 sec Number of successful tactic applications: 649 Number of failed tactic applications: 9352 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, 24 sec Number of successful tactic applications: 288 Number of failed tactic applications: 9713 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: 604 Original Proof: [by rewrite leqNgt.] Shorter Proof Found? no Proof reused from eqn_leq proof search time: 0 min, 1 sec Number of successful tactic applications: 10 Number of failed tactic applications: 594 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, 20 sec Number of successful tactic applications: 422 Number of failed tactic applications: 9579 Results for lemma subnn: : self_inverse 0 subn SUCCESS! Proof Found in EFSM: by elim. Tactics applied: 88 Original Proof: [by elim.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 12 Number of failed tactic applications: 76 Results for lemma lt_irrelevance: m n lt_mn1 lt_mn2 : lt_mn1 = lt_mn2 :> (m < n)%coq_nat FAILURE! Tactics applied: 320 Original Proof: [exact: (@le_irrelevance m.+1).] Proof search time: 0 min, 0 sec Number of successful tactic applications: 2 Number of failed tactic applications: 318 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: 1 min, 11 sec Number of successful tactic applications: 174 Number of failed tactic applications: 9827 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, 31 sec Number of successful tactic applications: 683 Number of failed tactic applications: 9318 Results for lemma addn_min_max: m n : minn m n + maxn m n = m + n FAILURE! Tactics applied: 1079 Original Proof: [by rewrite /minn /maxn; case: ltngtP => // [_|->] //; exact: addnC.] Proof search time: 0 min, 2 sec Number of successful tactic applications: 13 Number of failed tactic applications: 1066 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, 23 sec Number of successful tactic applications: 1567 Number of failed tactic applications: 8434 Results for lemma addSn: m n : m.+1 + n = (m + n).+1 SUCCESS! Proof Found in EFSM: split ; Tactics applied: 33 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: 30 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, 22 sec Number of successful tactic applications: 1037 Number of failed tactic applications: 8964 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, 22 sec Number of successful tactic applications: 244 Number of failed tactic applications: 9757 Results for lemma min0n: : left_zero 0 minn SUCCESS! Proof Found in EFSM: by case. Tactics applied: 57 Original Proof: [by case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 12 Number of failed tactic applications: 45 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, 26 sec Number of successful tactic applications: 378 Number of failed tactic applications: 9623 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, 21 sec Number of successful tactic applications: 811 Number of failed tactic applications: 9190 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, 16 sec Number of successful tactic applications: 830 Number of failed tactic applications: 9171 Results for lemma eqSS: m n : (m.+1 == n.+1) = (m == n) SUCCESS! Proof Found in EFSM: split ; Tactics applied: 33 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: 30 Results for lemma maxnK: m n : minn (maxn m n) m = m FAILURE! Tactics applied: 1019 Original Proof: [exact/minn_idPr/leq_maxl.] Proof search time: 0 min, 2 sec Number of successful tactic applications: 7 Number of failed tactic applications: 1012 Results for lemma find_ex_minn: : {m | P m & forall n, P n -> n >= m} FAILURE! Tactics applied: 318 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: 318 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 lemma expnS: m n : m ^ n.+1 = m * m ^ n SUCCESS! Proof Found in EFSM: elim : m n => [|m IHm] [|n] //; rewrite /ex_maxn; rewrite ?muln0; rewrite mulnSr muln0. exact : eqP. Tactics applied: 1434 Original Proof: [by case: n; rewrite ?muln1.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 3 sec Number of successful tactic applications: 26 Number of failed tactic applications: 1408 Results for lemma leqif_eq: m n : m <= n -> m <= n ?= iff (m == n) SUCCESS! Proof Found in EFSM: split => // j Pj. Tactics applied: 35 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: 20 Results for lemma eqb1: (b : bool) : (b == 1 :> nat) = b SUCCESS! Proof Found in EFSM: by case: b. Tactics applied: 62 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: 61 Results for lemma double_eq0: n : (n.*2 == 0) = (n == 0) SUCCESS! Proof Found in EFSM: by case: n. Tactics applied: 76 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: 73 Results for lemma doubleS: n : n.+1.*2 = n.*2.+2 SUCCESS! Proof Found in EFSM: split ; Tactics applied: 33 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: 30 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, 34 sec Number of successful tactic applications: 574 Number of failed tactic applications: 9427 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, 28 sec Number of successful tactic applications: 666 Number of failed tactic applications: 9335 Results for lemma odd_double: n : odd n.*2 = false SUCCESS! Proof Found in EFSM: by elim: n => //= n ->. Tactics applied: 104 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: 3 Number of failed tactic applications: 101 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: 382 Number of failed tactic applications: 9619 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, 17 sec Number of successful tactic applications: 1865 Number of failed tactic applications: 8136 Results for lemma odd_double_half: n : odd n + n./2.*2 = n FAILURE! Tactics applied: 319 Original Proof: [by elim: n => //= n {3}<-; rewrite uphalf_half doubleD; case (odd n).] Proof search time: 0 min, 0 sec Number of successful tactic applications: 2 Number of failed tactic applications: 317 Results for lemma eq_ex_minn: P Q exP exQ : P =1 Q -> @ex_minn P exP = @ex_minn Q exQ FAILURE! Tactics applied: 508 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, 1 sec Number of successful tactic applications: 10 Number of failed tactic applications: 498 Results for lemma iter_succn: m n : iter n succn m = m + n SUCCESS! Proof Found in EFSM: by elim: n => //= n ->. Tactics applied: 104 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: 5 Number of failed tactic applications: 99 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, 33 sec Number of successful tactic applications: 293 Number of failed tactic applications: 9708 Results for lemma mulnbl: (b : bool) n : b * n = (if b then n else 0) FAILURE! Tactics applied: 320 Original Proof: [by case: b; rewrite ?mul1n.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 2 Number of failed tactic applications: 318 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, 30 sec Number of successful tactic applications: 429 Number of failed tactic applications: 9572 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, 23 sec Number of successful tactic applications: 1170 Number of failed tactic applications: 8831 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, 30 sec Number of successful tactic applications: 428 Number of failed tactic applications: 9573 Results for lemma subn2: n : (n - 2)%N = n.-2 FAILURE! Tactics applied: 320 Original Proof: [by case: n => [|[|[]]].] Proof search time: 0 min, 0 sec Number of successful tactic applications: 2 Number of failed tactic applications: 318 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: 772 Original Proof: [by move/gtn_eqF; rewrite eq_sym.] Shorter Proof Found? no Proof reused from eqn_leq proof search time: 0 min, 2 sec Number of successful tactic applications: 28 Number of failed tactic applications: 744 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: 618 Original Proof: [by rewrite -doubleS leq_double.] Shorter Proof Found? no Proof reused from eqn_leq proof search time: 0 min, 2 sec Number of successful tactic applications: 20 Number of failed tactic applications: 598 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, 25 sec Number of successful tactic applications: 1184 Number of failed tactic applications: 8817 Results for lemma expnE: : expn = expn_rec SUCCESS! Proof Found in EFSM: split ; Tactics applied: 33 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: 32 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: 1301 Number of failed tactic applications: 8700 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, 22 sec Number of successful tactic applications: 893 Number of failed tactic applications: 9108 Results for lemma expn1: m : m ^ 1 = m SUCCESS! Proof Found in EFSM: split ; Tactics applied: 33 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: 32 Results for lemma subnDl: p m n : (p + m) - (p + n) = m - n SUCCESS! Proof Found in EFSM: by elim: p. Tactics applied: 120 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: 5 Number of failed tactic applications: 115 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, 16 sec Number of successful tactic applications: 2393 Number of failed tactic applications: 7608 Results for lemma eqn_add2l: p m n : (p + m == p + n) = (m == n) SUCCESS! Proof Found in EFSM: by elim: p. Tactics applied: 120 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: 5 Number of failed tactic applications: 115 Results for lemma ex_maxn_subproof: : exists i, P (m - i) FAILURE! Tactics applied: 318 Original Proof: [by case: exP => i Pi; exists (m - i); rewrite subKn ?ubP.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 318 Results for lemma uphalf_double: n : uphalf n.*2 = n SUCCESS! Proof Found in EFSM: by elim: n => //= n ->. Tactics applied: 104 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: 3 Number of failed tactic applications: 101 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, 25 sec Number of successful tactic applications: 885 Number of failed tactic applications: 9116 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, 20 sec Number of successful tactic applications: 890 Number of failed tactic applications: 9111 Results for lemma leP: m n : reflect (m <= n)%coq_nat (m <= n) FAILURE! Tactics applied: 1103 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, 2 sec Number of successful tactic applications: 12 Number of failed tactic applications: 1091 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: 618 Original Proof: [elim: m n => [|m IHm] [|n] //; exact: IHm n.] Shorter Proof Found? no Proof reused from eqn_leq proof search time: 0 min, 1 sec Number of successful tactic applications: 10 Number of failed tactic applications: 608 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: 2088 Number of failed tactic applications: 7913 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, 27 sec Number of successful tactic applications: 248 Number of failed tactic applications: 9753 Results for lemma subSS: n m : m.+1 - n.+1 = m - n SUCCESS! Proof Found in EFSM: split ; Tactics applied: 33 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: 30 Results for lemma maxKn: m n : minn n (maxn m n) = n FAILURE! Tactics applied: 1023 Original Proof: [exact/minn_idPl/leq_maxr.] Proof search time: 0 min, 2 sec Number of successful tactic applications: 11 Number of failed tactic applications: 1012 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, 23 sec Number of successful tactic applications: 2773 Number of failed tactic applications: 7228 Results for fold 3 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: 454 Number of failed tactic applications: 9547 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, 16 sec Number of successful tactic applications: 736 Number of failed tactic applications: 9265 Results for lemma addnK: n : cancel (addn^~ n) (subn^~ n) FAILURE! Tactics applied: 10000 Original Proof: [by move=> m; rewrite /= (addnC m) addKn.] Proof search time: 0 min, 15 sec Number of successful tactic applications: 696 Number of failed tactic applications: 9305 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, 21 sec Number of successful tactic applications: 955 Number of failed tactic applications: 9046 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: 334 Original Proof: [by rewrite -subnS.] Shorter Proof Found? no Proof reused from eqn_leq This proof contained a loop around a state proof search time: 0 min, 0 sec Number of successful tactic applications: 10 Number of failed tactic applications: 324 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, 15 sec Number of successful tactic applications: 262 Number of failed tactic applications: 9739 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, 28 sec Number of successful tactic applications: 846 Number of failed tactic applications: 9155 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, 20 sec Number of successful tactic applications: 616 Number of failed tactic applications: 9385 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, 19 sec Number of successful tactic applications: 447 Number of failed tactic applications: 9554 Results for lemma leq_addr: m n : n <= n + m SUCCESS! Proof Found in EFSM: by elim: n => // n IHn; Tactics applied: 120 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: 7 Number of failed tactic applications: 113 Results for lemma minnACA: : interchange minn minn SUCCESS! Proof Found in EFSM: move => Hmn; fix 2 => m IHm m_lb; by rewrite ?(mul1n, nat_of_addn_gt0, mulSn) //= !natTrecE IHp doubleMl. Tactics applied: 2970 Original Proof: [by move=> m n p q; rewrite -!minnA (minnCA n).] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 4 sec Number of successful tactic applications: 144 Number of failed tactic applications: 2826 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: 334 Original Proof: [by rewrite eqn_leq (leqNgt n) => ->.] Shorter Proof Found? no Proof reused from eqn_leq This proof contained a loop around a state proof search time: 0 min, 0 sec Number of successful tactic applications: 22 Number of failed tactic applications: 312 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: 913 Number of failed tactic applications: 9088 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) SUCCESS! Proof Found in EFSM: move => Hmn; fix 2 => m IHm m_lb; by case: (odd m); Tactics applied: 2479 Original Proof: [by move=> f_mono m n C; rewrite /leqif !eqn_leq !f_mono.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 4 sec Number of successful tactic applications: 114 Number of failed tactic applications: 2365 Results for lemma iter_succn_0: n : iter n succn 0 = n SUCCESS! Proof Found in EFSM: by elim: n => //= n ->. Tactics applied: 122 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: 4 Number of failed tactic applications: 118 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, 14 sec Number of successful tactic applications: 298 Number of failed tactic applications: 9703 Results for lemma leqn0: n : (n <= 0) = (n == 0) 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, 0 sec Number of successful tactic applications: 4 Number of failed tactic applications: 93 Results for lemma eqb0: (b : bool) : (b == 0 :> nat) = ~~ 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, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 76 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: 538 Number of failed tactic applications: 9463 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, 23 sec Number of successful tactic applications: 840 Number of failed tactic applications: 9161 Results for lemma eqn_sqr: m n : (m ^ 2 == n ^ 2) = (m == n) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite eqn_exp2r.] Proof search time: 0 min, 26 sec Number of successful tactic applications: 996 Number of failed tactic applications: 9005 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, 25 sec Number of successful tactic applications: 615 Number of failed tactic applications: 9386 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: 122 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: 7 Number of failed tactic applications: 115 Results for lemma leqnSn: n : n <= n.+1 SUCCESS! Proof Found in EFSM: by elim: n => // n IHn; Tactics applied: 120 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: 4 Number of failed tactic applications: 116 Results for lemma sub1b: (b : bool) : 1 - b = ~~ 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, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 76 Results for lemma minnn: : idempotent minn FAILURE! Tactics applied: 10000 Original Proof: [by move=> n; apply/minn_idPl.] Proof search time: 0 min, 14 sec Number of successful tactic applications: 685 Number of failed tactic applications: 9316 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, 26 sec Number of successful tactic applications: 1236 Number of failed tactic applications: 8765 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, 25 sec Number of successful tactic applications: 818 Number of failed tactic applications: 9183 Results for lemma exp1n: n : 1 ^ n = 1 FAILURE! Tactics applied: 10000 Original Proof: [by elim: n => // n; rewrite expnS mul1n.] Proof search time: 0 min, 16 sec Number of successful tactic applications: 2690 Number of failed tactic applications: 7311 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, 19 sec Number of successful tactic applications: 543 Number of failed tactic applications: 9458 Results for lemma leqSpred: n : n <= n.-1.+1 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, 0 sec Number of successful tactic applications: 4 Number of failed tactic applications: 93 Results for lemma odd_gt2: n : odd n -> n > 1 -> n > 2 SUCCESS! Proof Found in EFSM: by case: n => [|[|[]]]. Tactics applied: 99 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: 23 Number of failed tactic applications: 76 Results for lemma maxnn: : idempotent maxn FAILURE! Tactics applied: 10000 Original Proof: [by move=> n; apply/maxn_idPl.] Proof search time: 0 min, 14 sec Number of successful tactic applications: 697 Number of failed tactic applications: 9304 Results for lemma factS: n : (n.+1)`! = n.+1 * n`! SUCCESS! Proof Found in EFSM: split ; Tactics applied: 11 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: 8 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, 17 sec Number of successful tactic applications: 441 Number of failed tactic applications: 9560 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: 115 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: 95 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, 24 sec Number of successful tactic applications: 526 Number of failed tactic applications: 9475 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, 17 sec Number of successful tactic applications: 441 Number of failed tactic applications: 9560 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, 16 sec Number of successful tactic applications: 302 Number of failed tactic applications: 9699 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, 23 sec Number of successful tactic applications: 480 Number of failed tactic applications: 9521 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: 332 Original Proof: [by elim: m n => [|m IHm] [|n] //; exact: IHm n.] Shorter Proof Found? no Proof reused from eqn_leq This proof contained a loop around a state proof search time: 0 min, 0 sec Number of successful tactic applications: 10 Number of failed tactic applications: 322 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, 15 sec Number of successful tactic applications: 440 Number of failed tactic applications: 9561 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, 22 sec Number of successful tactic applications: 964 Number of failed tactic applications: 9037 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, 24 sec Number of successful tactic applications: 831 Number of failed tactic applications: 9170 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, 23 sec Number of successful tactic applications: 1222 Number of failed tactic applications: 8779 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: 334 Original Proof: [by move=> lemn; split=> //; rewrite eqn_leq lemn.] Shorter Proof Found? yes Proof reused from eqn_leq This proof contained a loop around a state proof search time: 0 min, 1 sec Number of successful tactic applications: 35 Number of failed tactic applications: 299 Results for lemma eq_iter: f f' : f =1 f' -> forall n, iter n f =1 iter 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, 14 sec Number of successful tactic applications: 244 Number of failed tactic applications: 9757 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, 18 sec Number of successful tactic applications: 395 Number of failed tactic applications: 9606 Results for lemma addn3: m : m + 3 = m.+3 SUCCESS! Proof Found in EFSM: exact : addnC. Tactics applied: 25 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: 1 Number of failed tactic applications: 24 Results for lemma leqnn: n : n <= n SUCCESS! Proof Found in EFSM: by elim: n => // n IHn; Tactics applied: 120 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: 4 Number of failed tactic applications: 116 Results for lemma odd_gt0: n : odd n -> n > 0 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, 0 sec Number of successful tactic applications: 16 Number of failed tactic applications: 81 Results for lemma muln0: : right_zero 0 muln SUCCESS! Proof Found in EFSM: by []. 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: 17 Number of failed tactic applications: 50 Results for lemma neq0_lt0n: n : (n == 0) = false -> 0 < 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, 0 sec Number of successful tactic applications: 16 Number of failed tactic applications: 81 Results for lemma minn0: : right_zero 0 minn SUCCESS! Proof Found in EFSM: split ; Tactics applied: 11 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: 10 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: 1831 Number of failed tactic applications: 8170 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, 15 sec Number of successful tactic applications: 679 Number of failed tactic applications: 9322 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, 21 sec Number of successful tactic applications: 559 Number of failed tactic applications: 9442 Results for lemma muln2: m : m * 2 = m.*2 FAILURE! Tactics applied: 3489 Original Proof: [by rewrite mulnC mul2n.] Proof search time: 0 min, 5 sec Number of successful tactic applications: 53 Number of failed tactic applications: 3436 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: 2 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: 1 Number of failed tactic applications: 1 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, 15 sec Number of successful tactic applications: 685 Number of failed tactic applications: 9316 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, 20 sec Number of successful tactic applications: 906 Number of failed tactic applications: 9095 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, 18 sec Number of successful tactic applications: 411 Number of failed tactic applications: 9590 Results for lemma le_irrelevance: m n le_mn1 le_mn2 : le_mn1 = le_mn2 :> (m <= n)%coq_nat FAILURE! Tactics applied: 2874 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, 3 sec Number of successful tactic applications: 38 Number of failed tactic applications: 2836 Results for lemma subn1: n : n - 1 = n.-1 SUCCESS! Proof Found in EFSM: by case: n => [|[|[]]]. Tactics applied: 99 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: 4 Number of failed tactic applications: 95 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, 20 sec Number of successful tactic applications: 1020 Number of failed tactic applications: 8981 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, 19 sec Number of successful tactic applications: 1083 Number of failed tactic applications: 8918 Results for lemma double0: : 0.*2 = 0 SUCCESS! Proof Found in EFSM: split ; Tactics applied: 11 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: 10 Results for lemma mul1n: : left_id 1 muln FAILURE! Tactics applied: 10000 Original Proof: [exact: addn0.] Proof search time: 0 min, 15 sec Number of successful tactic applications: 721 Number of failed tactic applications: 9280 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: 122 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: 4 Number of failed tactic applications: 118 Results for fold 4 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: 1172 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: 61 Number of failed tactic applications: 1111 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, 21 sec Number of successful tactic applications: 511 Number of failed tactic applications: 9490 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, 18 sec Number of successful tactic applications: 394 Number of failed tactic applications: 9607 Results for lemma sqrn_inj: : injective (expn ^~ 2) FAILURE! Tactics applied: 10000 Original Proof: [exact: expIn.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 2276 Number of failed tactic applications: 7725 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, 22 sec Number of successful tactic applications: 776 Number of failed tactic applications: 9225 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, 27 sec Number of successful tactic applications: 1044 Number of failed tactic applications: 8957 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, 23 sec Number of successful tactic applications: 720 Number of failed tactic applications: 9281 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, 21 sec Number of successful tactic applications: 1507 Number of failed tactic applications: 8494 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, 27 sec Number of successful tactic applications: 631 Number of failed tactic applications: 9370 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] //; rewrite /ex_maxn; rewrite (muln0, mulnS) // mulSn => ->. Tactics applied: 8354 Original Proof: [by case: m n => // m [|n] //=; rewrite muln0.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 21 sec Number of successful tactic applications: 501 Number of failed tactic applications: 7853 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: 726 Number of failed tactic applications: 9275 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; elim : n => //= n ->; by do 2!case: odd; Tactics applied: 5235 Original Proof: [by elim=> //= n ->.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 10 sec Number of successful tactic applications: 202 Number of failed tactic applications: 5033 Results for lemma addnC: : commutative addn FAILURE! Tactics applied: 10000 Original Proof: [by move=> m n; rewrite -{1}[n]addn0 addnCA addn0.] Proof search time: 0 min, 15 sec Number of successful tactic applications: 353 Number of failed tactic applications: 9648 Results for lemma ltn0: n : n < 0 = false 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, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 0 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: 766 Number of failed tactic applications: 9235 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, 27 sec Number of successful tactic applications: 690 Number of failed tactic applications: 9311 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, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 0 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: 671 Number of failed tactic applications: 9330 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: 1173 Original Proof: [by rewrite /leq -doubleB; case (m - n).] Shorter Proof Found? no Proof reused from doubleB proof search time: 0 min, 2 sec Number of successful tactic applications: 55 Number of failed tactic applications: 1118 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, 22 sec Number of successful tactic applications: 685 Number of failed tactic applications: 9316 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, 23 sec Number of successful tactic applications: 774 Number of failed tactic applications: 9227 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, 20 sec Number of successful tactic applications: 489 Number of failed tactic applications: 9512 Results for lemma eq_iterop: n op op' : op =2 op' -> iterop n op =2 iterop n op' FAILURE! Tactics applied: 10000 Original Proof: [by move=> eq_op x; apply: eq_iteri; case.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 1396 Number of failed tactic applications: 8605 Results for lemma half_gt0: n : (0 < n./2) = (1 < n) 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: 9 Number of failed tactic applications: 132 Results for lemma add4n: m : 4 + m = m.+4 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, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 0 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, 28 sec Number of successful tactic applications: 760 Number of failed tactic applications: 9241 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, 20 sec Number of successful tactic applications: 395 Number of failed tactic applications: 9606 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, 17 sec Number of successful tactic applications: 428 Number of failed tactic applications: 9573 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, 24 sec Number of successful tactic applications: 747 Number of failed tactic applications: 9254 Results for lemma addSnnS: m n : m.+1 + n = m + n.+1 FAILURE! Tactics applied: 10000 Original Proof: [by rewrite addnS.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 363 Number of failed tactic applications: 9638 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, 23 sec Number of successful tactic applications: 679 Number of failed tactic applications: 9322 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, 22 sec Number of successful tactic applications: 505 Number of failed tactic applications: 9496 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, 22 sec Number of successful tactic applications: 765 Number of failed tactic applications: 9236 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, 23 sec Number of successful tactic applications: 730 Number of failed tactic applications: 9271 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: 1161 Original Proof: [by rewrite ltnNge leq_eqVlt negb_or -leqNgt eq_sym.] Shorter Proof Found? no Proof reused from doubleB proof search time: 0 min, 2 sec Number of successful tactic applications: 53 Number of failed tactic applications: 1108 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: 543 Number of failed tactic applications: 9458 Results for lemma mulSn: m n : m.+1 * n = n + m * n 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, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 0 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, 19 sec Number of successful tactic applications: 356 Number of failed tactic applications: 9645 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, 28 sec Number of successful tactic applications: 782 Number of failed tactic applications: 9219 Results for lemma mulnbr: (b : bool) n : n * b = (if b then n else 0) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite mulnC mulnbl.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 395 Number of failed tactic applications: 9606 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, 23 sec Number of successful tactic applications: 622 Number of failed tactic applications: 9379 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, 19 sec Number of successful tactic applications: 358 Number of failed tactic applications: 9643 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, 22 sec Number of successful tactic applications: 432 Number of failed tactic applications: 9569 Results for lemma add0n: : left_id 0 addn 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, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 0 Results for lemma subn_eq0: m n : (m - n == 0) = (m <= n) 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, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 0 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, 22 sec Number of successful tactic applications: 1267 Number of failed tactic applications: 8734 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: 1169 Original Proof: [by rewrite -subn_eq0 -subnDA.] Shorter Proof Found? no Proof reused from doubleB proof search time: 0 min, 2 sec Number of successful tactic applications: 53 Number of failed tactic applications: 1116 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, 23 sec Number of successful tactic applications: 718 Number of failed tactic applications: 9283 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: 429 Number of failed tactic applications: 9572 Results for lemma addn_negb: (b : bool) : ~~ b + b = 1 SUCCESS! Proof Found in EFSM: by case: b. Tactics applied: 121 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: 118 Results for lemma fact0: : 0`! = 1 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, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 0 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, 26 sec Number of successful tactic applications: 1109 Number of failed tactic applications: 8892 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, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 0 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: 615 Number of failed tactic applications: 9386 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, 24 sec Number of successful tactic applications: 757 Number of failed tactic applications: 9244 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, 22 sec Number of successful tactic applications: 670 Number of failed tactic applications: 9331 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: 436 Number of failed tactic applications: 9565 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, 22 sec Number of successful tactic applications: 559 Number of failed tactic applications: 9442 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, 21 sec Number of successful tactic applications: 312 Number of failed tactic applications: 9689 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, 20 sec Number of successful tactic applications: 399 Number of failed tactic applications: 9602 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: 384 Number of failed tactic applications: 9617 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, 21 sec Number of successful tactic applications: 376 Number of failed tactic applications: 9625 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: 1151 Original Proof: [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: 53 Number of failed tactic applications: 1098 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, 25 sec Number of successful tactic applications: 655 Number of failed tactic applications: 9346 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, 28 sec Number of successful tactic applications: 344 Number of failed tactic applications: 9657 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: 1848 Number of failed tactic applications: 8153 Results for lemma double_gt0: n : (0 < n.*2) = (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: 9 Number of failed tactic applications: 130 Results for lemma nat_of_add_bin: b1 b2 : (b1 + b2)%num = b1 + b2 :> nat FAILURE! Tactics applied: 10000 Original Proof: [case: b1 b2 => [|p] [|q] //=; exact: nat_of_addn_gt0.] Proof search time: 0 min, 29 sec Number of successful tactic applications: 512 Number of failed tactic applications: 9489 Results for lemma addKn: n : cancel (addn n) (subn^~ n) SUCCESS! Proof Found in EFSM: elim : n => [|n IHn]. case => //=. rewrite ?expn1 // ltn_mul // IHe. Tactics applied: 5885 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, 10 sec Number of successful tactic applications: 268 Number of failed tactic applications: 5617 Results for fold 5 Results for lemma addn2: m : m + 2 = m.+2 SUCCESS! Proof Found in EFSM: by rewrite addnC. Tactics applied: 232 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: 229 Results for lemma eq_leq: m n : m = n -> m <= n SUCCESS! Proof Found in EFSM: by elim. Tactics applied: 88 Original Proof: [by move->.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 14 Number of failed tactic applications: 74 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, 18 sec Number of successful tactic applications: 606 Number of failed tactic applications: 9395 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, 18 sec Number of successful tactic applications: 1022 Number of failed tactic applications: 8979 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, 21 sec Number of successful tactic applications: 458 Number of failed tactic applications: 9543 Results for lemma iterS: n f x : iter n.+1 f x = f (iter n f x) SUCCESS! Proof Found in EFSM: split ; Tactics applied: 31 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: 30 Results for lemma leq0n: n : 0 <= n SUCCESS! Proof Found in EFSM: split ; Tactics applied: 31 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: 30 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: 228 Number of failed tactic applications: 9773 Results for lemma add1n: n : 1 + n = n.+1 SUCCESS! Proof Found in EFSM: split ; Tactics applied: 31 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: 30 Results for lemma addn_eq0: m n : (m + n == 0) = (m == 0) && (n == 0) SUCCESS! Proof Found in EFSM: by case: m => [|[|m]] // _; Tactics applied: 71 Original Proof: [by case: m; case: n.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 6 Number of failed tactic applications: 65 Results for lemma lt0n: n : (0 < n) = (n != 0) SUCCESS! Proof Found in EFSM: by case: n. Tactics applied: 77 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: 72 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, 22 sec Number of successful tactic applications: 483 Number of failed tactic applications: 9518 Results for lemma add2n: m : 2 + m = m.+2 SUCCESS! Proof Found in EFSM: split ; Tactics applied: 31 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: 30 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, 18 sec Number of successful tactic applications: 540 Number of failed tactic applications: 9461 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, 21 sec Number of successful tactic applications: 434 Number of failed tactic applications: 9567 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, 26 sec Number of successful tactic applications: 701 Number of failed tactic applications: 9300 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, 28 sec Number of successful tactic applications: 337 Number of failed tactic applications: 9664 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, 25 sec Number of successful tactic applications: 495 Number of failed tactic applications: 9506 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, 21 sec Number of successful tactic applications: 1003 Number of failed tactic applications: 8998 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: 108 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: 5 Number of failed tactic applications: 103 Results for lemma eqnE: : eqn = eq_op SUCCESS! Proof Found in EFSM: split ; Tactics applied: 31 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: 30 Results for lemma addn_gt0: m n : (0 < m + n) = (0 < m) || (0 < n) SUCCESS! Proof Found in EFSM: by case: m => [|[|m]] // _; Tactics applied: 71 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: 6 Number of failed tactic applications: 65 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, 20 sec Number of successful tactic applications: 936 Number of failed tactic applications: 9065 Results for lemma leqif_refl: m C : reflect (m <= m ?= iff C) C SUCCESS! Proof Found in EFSM: have sub2nn n : n.*2 - n = n by rewrite -addnn addKn. apply : (iffP idP) => [|<-]; by elim: m. Tactics applied: 448 Original Proof: [by apply: (iffP idP) => [-> | <-] //; split; rewrite ?eqxx.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 1 sec Number of successful tactic applications: 9 Number of failed tactic applications: 439 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, 26 sec Number of successful tactic applications: 789 Number of failed tactic applications: 9212 Results for lemma succnK: : cancel succn predn SUCCESS! Proof Found in EFSM: split ; Tactics applied: 31 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 11 Number of failed tactic applications: 20 Results for lemma mul0n: : left_zero 0 muln SUCCESS! Proof Found in EFSM: split ; Tactics applied: 31 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 11 Number of failed tactic applications: 20 Results for lemma nat_of_succ_gt0: p : Psucc p = p.+1 :> nat FAILURE! Tactics applied: 637 Original Proof: [by elim: p => //= p ->; rewrite !natTrecE.] Proof search time: 0 min, 1 sec Number of successful tactic applications: 16 Number of failed tactic applications: 621 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, 19 sec Number of successful tactic applications: 487 Number of failed tactic applications: 9514 Results for lemma addnE: : addn = addn_rec SUCCESS! Proof Found in EFSM: split ; Tactics applied: 31 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: 30 Results for lemma succn_inj: : injective succn SUCCESS! Proof Found in EFSM: move => le1 le2; case => //= n; Tactics applied: 499 Original Proof: [by move=> n m [].] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 1 sec Number of successful tactic applications: 39 Number of failed tactic applications: 460 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, 21 sec Number of successful tactic applications: 962 Number of failed tactic applications: 9039 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, 29 sec Number of successful tactic applications: 1192 Number of failed tactic applications: 8809 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: 957 Original Proof: [by rewrite 2!ltnNge leq_double.] Shorter Proof Found? no Proof reused from leq_eqVlt proof search time: 0 min, 2 sec Number of successful tactic applications: 59 Number of failed tactic applications: 898 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: 957 Original Proof: [by rewrite leqNgt ltn_Sdouble -leqNgt.] Shorter Proof Found? no Proof reused from leq_eqVlt proof search time: 0 min, 2 sec Number of successful tactic applications: 47 Number of failed tactic applications: 910 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: 957 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, 2 sec Number of successful tactic applications: 41 Number of failed tactic applications: 916 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, 18 sec Number of successful tactic applications: 638 Number of failed tactic applications: 9363 Results for lemma leq_ltn_trans: n m p : m <= n -> n < p -> m < p FAILURE! Tactics applied: 10000 Original Proof: [move=> Hmn; exact: leq_trans.] Proof search time: 0 min, 26 sec Number of successful tactic applications: 755 Number of failed tactic applications: 9246 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, 22 sec Number of successful tactic applications: 669 Number of failed tactic applications: 9332 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, 28 sec Number of successful tactic applications: 444 Number of failed tactic applications: 9557 Results for lemma leq_add2l: p m n : (p + m <= p + n) = (m <= n) SUCCESS! Proof Found in EFSM: by elim: p. Tactics applied: 120 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: 6 Number of failed tactic applications: 114 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, 19 sec Number of successful tactic applications: 716 Number of failed tactic applications: 9285 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, 18 sec Number of successful tactic applications: 606 Number of failed tactic applications: 9395 Results for lemma addn1: n : n + 1 = n.+1 SUCCESS! Proof Found in EFSM: by rewrite addnC. Tactics applied: 231 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: 226 Results for lemma eq_iteri: f f' : f =2 f' -> forall n, iteri n f =1 iteri n f' FAILURE! Tactics applied: 2355 Original Proof: [by move=> eq_f n x; elim: n => //= n ->; rewrite eq_f.] Proof search time: 0 min, 4 sec Number of successful tactic applications: 60 Number of failed tactic applications: 2295 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, 25 sec Number of successful tactic applications: 447 Number of failed tactic applications: 9554 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, 17 sec Number of successful tactic applications: 1964 Number of failed tactic applications: 8037 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, 29 sec Number of successful tactic applications: 554 Number of failed tactic applications: 9447 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, 18 sec Number of successful tactic applications: 617 Number of failed tactic applications: 9384 Results for lemma lt0b: (b : bool) : (b > 0) = b SUCCESS! Proof Found in EFSM: by case: b. Tactics applied: 63 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: 60 Results for lemma ltn_add2l: p m n : (p + m < p + n) = (m < n) SUCCESS! Proof Found in EFSM: by elim: p. Tactics applied: 120 Original Proof: [by rewrite -addnS; exact: leq_add2l.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 6 Number of failed tactic applications: 114 Results for lemma muln_eq0: m n : (m * n == 0) = (m == 0) || (n == 0) 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: 537 Number of failed tactic applications: 9464 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: 1274 Number of failed tactic applications: 8727 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, 20 sec Number of successful tactic applications: 809 Number of failed tactic applications: 9192 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, 17 sec Number of successful tactic applications: 586 Number of failed tactic applications: 9415 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, 22 sec Number of successful tactic applications: 551 Number of failed tactic applications: 9450 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, 20 sec Number of successful tactic applications: 1043 Number of failed tactic applications: 8958 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: 338 Number of failed tactic applications: 9663 Results for lemma nat_of_addn_gt0: p q : (p + q)%positive = p + q :> nat FAILURE! Tactics applied: 625 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, 1 sec Number of successful tactic applications: 15 Number of failed tactic applications: 610 Results for lemma plusE: : plus = addn SUCCESS! Proof Found in EFSM: split ; Tactics applied: 31 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: 30 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, 21 sec Number of successful tactic applications: 434 Number of failed tactic applications: 9567 Results for lemma subn0: : right_id 0 subn SUCCESS! Proof Found in EFSM: case => //=; Tactics applied: 54 Original Proof: [by case.] 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: 41 Results for lemma addn0: : right_id 0 addn SUCCESS! Proof Found in EFSM: case => //=; Tactics applied: 54 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: 13 Number of failed tactic applications: 41 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, 21 sec Number of successful tactic applications: 1005 Number of failed tactic applications: 8996 Results for lemma ltnW: m n : m < n -> m <= n SUCCESS! Proof Found in EFSM: elim : m n => [|m IHm] [|n] //; exact : IHm n. Tactics applied: 1242 Original Proof: [exact: leq_trans.] Shorter Proof Found? no Proof reused from leq_eqVlt proof search time: 0 min, 3 sec Number of successful tactic applications: 85 Number of failed tactic applications: 1157 OVERALL RESULTS SUMMARY EFSMProver proved 131 out of 341 lemmas. Success rate of 38.41642228739003% There were 0 errors. 209 proof attempts exhausted the automaton On average, a proof was found after applying 395 tactics The longest proof consisted of 5 tactics There were 9 shorter proofs found Of the 209 failures, 192 of them used all 10000 tactics There were 117 reused proofs found There were 14 novel proofs found Of the 209 failures, the average number of tactics used was 9267 On average, a proof was found after 0 min, 1 sec On average, a failed proof attempt took 0 min, 20 sec On average, any (success or failure) proof attempt took 0 min, 13 sec The longest time to find a proof was 0 min, 21 sec The shortest time to find a proof was 0 min, 0 sec There were 0 proofs containing repeated tactics There were 7 proofs that repeated states