proposition: Theorem lt_diff : forall a b : A, lt a b -> a <> b.
proof: Proof. unfold A, lt, le in |- *; intros a b; case a; case b. simple destruct 1. intro H0; red in |- *; injection 1. intros e1 e2; rewrite e2 in H0. case (M1.lt_irreflexive a0 H0). simple destruct 1. simple destruct 1. intro H2; red in |- *; injection 1. intro e; rewrite e in H2; case (M2.lt_irreflexive _ H2). Qed.
imports: Relations List ZArith