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. simple destruct 1; intros; auto. right; case H0; split; auto. apply D2.lt_le_weak; trivial. Qed.
imports: Relations List ZArith