proposition: Lemma mult_cancel_less : forall x y z : R, [0] [<] z -> x[*]z [<] y[*]z -> x [<] y.
proof: Proof. intros x y z H H0. generalize (Greater_imp_ap _ _ _ H); intro H1. rstepl (x[*]z[*]([1][/] z[//]H1)). rstepr (y[*]z[*]([1][/] z[//]H1)). apply mult_resp_less. assumption. rstepl ([0][/] z[//]H1). apply div_resp_less_rht. apply pos_one. assumption. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)