proposition: Theorem le_lt_or_eq : forall a b:A, le a b -> lt a b \/ a = b.
proof: Proof. induction a as [ |x l IHl]; destruct b; simpl. - auto. - auto. - contradiction. - intros [H | [H0 H1]]. + left; auto. + destruct (IHl _ H1). * left;auto. * subst b a; right; auto. Qed.
imports: DecOrders