proposition: Theorem le_lt_or_eq : forall a b:A, a <= b -> a < b \/ a = b.
proof: Proof. intros a b; case a; case b. - intros a0 a1 H; case (O1.le_lt_or_eq a1 a0 H); auto. intro e; subst a1; auto. - left. constructor. - inversion 1. - intros a0 a1 H; case (O2.le_lt_or_eq a1 a0 H); auto. intro; subst a1;now right. Qed.
imports: Relations List ZArith