proposition: Lemma mult_cancel_leEq : forall x y z : R, [0] [<] z -> x[*]z [<=] y[*]z -> x [<=] y.
proof: Proof. intros x y z H. do 2 rewrite -> leEq_def. intros H0 H1. apply H0. apply mult_resp_less. assumption. assumption. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)