reflexivity.
qed.
+
+lemma orb_false_false :
+ ∀b1,b2:bool.((or_bool b1 b2) = false) → b1 = false.
+ intros 2;
+ elim b1 0;
+ elim b2;
+ simplify in H;
+ try destruct H;
+ reflexivity.
+qed.
+
+lemma orb_false_false_r :
+ ∀b1,b2:bool.((or_bool b1 b2) = false) → b2 = false.
+ intros 2;
+ elim b1 0;
+ elim b2;
+ simplify in H;
+ try destruct H;
+ reflexivity.
+qed.
+
lemma eqbool_to_eq : ∀b1,b2:bool.(eq_bool b1 b2 = true) → (b1 = b2).
unfold eq_bool;
intros;
lemma le_to_lt: ∀n,m. n ≤ m → n < S m.
intros;
- autobatch.
+ unfold;autobatch.
qed.
alias num (instance 0) = "natural number".
]
| elim H1; autobatch
]
- | autobatch
+ | exists;[apply (pred m);]autobatch
].
qed.