proposition: Lemma mult_cancel_pos_rht : forall x y : R, [0] [<] x[*]y -> [0] [<=] x -> [0] [<] y.
proof: Proof. intros x y H. destruct (leEq_def _ [0] x) as [H0 _]. intro H2. pose (H3:=(H0 H2)). elim (mult_pos_imp _ _ H); intro H1. elim H1; auto. elim H1; intros. contradiction. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)