proposition: Lemma swap_div : forall (x y z : R) y_ z_, [0] [<] y -> [0] [<] z -> (x[/] z[//]z_) [<] y -> (x[/] y[//]y_) [<] z.
proof: Proof. intros. rstepl ((x[/] z[//]z_)[*](z[/] y[//]y_)). astepr (y[*](z[/] y[//]y_)). apply mult_resp_less. auto. apply div_resp_pos; auto. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)