proposition: Theorem le_lt_or_eq : forall a b : A, le a b -> lt a b \/ a = b.
proof: Proof. unfold A, lt, le in |- *; intros a b; case a; case b. intros a0 a1 H; case (O1.le_lt_or_eq a1 a0 H). auto. simple destruct 1; auto. auto. contradiction. intros a0 a1 H; case (O2.le_lt_or_eq a1 a0 H); auto. simple destruct 1; auto. Qed.
imports: Relations List ZArith