proposition: Theorem lt_not_le : forall a b : A, lt a b -> ~ le b a.
proof: Proof. intros a b H H0. absurd (a = b). apply D.lt_diff; trivial. apply le_antisym; auto; apply D.lt_le_weak; assumption. Qed.
imports: Relations List ZArith