proposition: Theorem le_lt_or_eq : forall a b:A, le a b -> lt a b \/ a = b.
proof: Proof. unfold lt, le ; intros a b; case a; case b. simple destruct 1; auto. simple destruct 1. simple destruct 1. intro H2; case (D2.le_lt_or_eq _ _ H2). - auto. - simple destruct 1; auto. Qed.
imports: Relations List ZArith