proposition: Lemma inv_resp_leEq : forall x y : R, x [<=] y -> [--]y [<=] [--]x.
proof: Proof. intros x y. repeat rewrite -> leEq_def. do 2 intro. apply H. apply inv_cancel_less. assumption. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)