*)
(* some basic properties of and - or*)
-theorem andb_sym: \forall A,B:bool.
+(*theorem andb_sym: \forall A,B:bool.
(A \land B) = (B \land A).
intros.
elim A;
rewrite > H2.
reflexivity.
qed.
-
+*)
(*properties about relational operators*)
theorem Sa_le_b_to_O_lt_b: \forall a,b:nat.
apply lt_O_S.
qed.
+
theorem n_gt_Uno_to_O_lt_pred_n: \forall n:nat.
(S O) \lt n \to O \lt (pred n).
intros.