proposition: Theorem lt_le_weak : forall a b : A, lt a b -> le a b.
proof: Proof. unfold A, lt, le in |- *; intros a b. case a; case b; auto. intros; apply O1.lt_le_weak; trivial. intros; apply O2.lt_le_weak; trivial. Qed.
imports: Relations List ZArith