proposition: Lemma test_autorename: forall x y, 0 <= 1 -> (0%Z <= 1%Z)%Z -> x <= y -> x = y -> 0 = 1 -> (0 = 1)%Z -> ~x = y -> true = Nat.eqb 3 4 -> Nat.eqb 3 4 = true -> true = Nat.leb 3 4 -> 1 = 0 -> ~x = y -> ~1 < 0 -> (forall w w':nat , w = w' -> ~true=false) -> (forall w w':nat , w = w' -> true=false /\ True) -> (forall w w':nat , w = w' -> False /\ True) -> (exists w:nat , w = w -> ~(true=(andb false true)) /\ False) -> (exists w:nat , w = w -> True /\ False) -> (forall w w':nat , w = w' -> true=false) -> (forall w w':nat , w = w' -> Nat.eqb 3 4=Nat.eqb 4 3) -> List.length (cons 3 nil) = (fun x => 0)1 -> List.length (cons 3 nil) = 0 -> plus 0 y = y -> (true=false) -> (False -> (true=false)) -> forall (x : nat) (env : list nat), ~ List.In x nil -> cons x (cons 3 env) = cons 2 env -> forall z t:nat, IDProp -> (0 < 1 -> 0 < 0 -> true = false -> ~(true=false)) -> (~(true=false)) -> (forall w w',w < w' -> ~(true=false)) -> (0 < 1 -> ~(1<0)) -> (0 < 1 -> 1<0) -> 0 < z -> True.
proof: Proof. intros /n. test x nat. test y nat. test h_le_0_1_ (0 <= 1). test h_le_0_1_0 ((0 <= 1)%Z). test h_le_x_y_ (x <= y). test h_eq_x_y_ (x = y). test h_eq_0_1_ (0 = 1). test h_eq_0_1_0 (0%Z = 1%Z). test h_neq_x_y_ (x <> y). test h_Neqb_3_4_ (true = (3 =? 4)). test h_Neqb_3_4_0 ((3 =? 4) = true). test h_eq_true_leb_3_4_ (true = (3 <=? 4)). test h_eq_1_0_ (1 = 0). test h_neq_x_y_ (x <> y). test h_not_lt_1_0_ (~ 1 < 0). test h_all_tNEQf_ (forall w w' : nat, w = w' -> true <> false). test h_all_and_tEQf_True_ (forall w w' : nat, w = w' -> true = false /\ True). test h_all_and_False_True_ (forall w w' : nat, w = w' -> False /\ True). test h_ex_and_neq_False_ (exists w : nat, w = w -> true <> (false && true)%bool /\ False). test h_ex_and_True_False_ (exists w : nat, w = w -> True /\ False). test h_all_tEQf_ (forall w w' : nat, w = w' -> true = false). test h_all_eq_eqb_eqb_ (forall w w' : nat, w = w' -> (3 =? 4) = (4 =? 3)). test h_eq_length_cons_ (length [3] = (fun _ : nat => 0) 1). test h_eq_length_cons_0_ (length [3] = 0). test h_eq_add_0_y_y_ (0 + y = y). test h_tEQf_ (true = false). test h_impl_tEQf_ (False -> true = false). test x0 (nat). test env (list nat). test h_not_In_x0_nil_ (~ In x0 []). test h_eq_cons_x0_3_cons_2_ (x0 :: 3 :: env = 2 :: env). test h_IDProp_ (IDProp). test h_impl_tNEQf_ (0 < 1 -> 0 < 0 -> true = false -> true <> false). test h_tNEQf_ (true <> false). test h_all_tNEQf_0 ((forall w w' : nat, w < w' -> true <> false)). test h_impl_not_lt_ (0 < 1 -> ~ 1 < 0). test h_impl_lt_1_0_ (0 < 1 -> 1 < 0). test h_lt_0_z_ (0 < z). exact I. Qed.
imports: Arith ZArith LibHyps.LibHyps List