proposition: Theorem lt_diff : forall a b : A, lt a b -> a <> b.
proof: Proof. unfold lt in |- *; simple destruct a; simple destruct b. intros a1 H e; injection e; intro e'. case (O1.lt_diff _ _ H e'). intros a1 H e; discriminate e. contradiction. intros a1 H e; injection e; intro e'. case (O2.lt_diff _ _ H e'). Qed.
imports: Relations List ZArith