proposition: Theorem lt_le_weak : forall a b:A, lt a b -> le a b.
proof: Proof. Proof Nat.lt_le_incl. Theorem lt_diff : forall a b:A, lt a b -> a <> b. Proof. unfold lt, le in |- *; intros a b H e; rewrite e in H; case (Nat.lt_irrefl b H). Qed.
imports: Relations List ZArith Arith