proposition: Lemma inv_lt_mono p q : p < q ↔ /q < /p.
proof: Proof. revert p q. cut (∀ p q, p < q → / q < / p). { intros help p q. split; [apply help|]. intros. rewrite <-(inv_involutive p), <-(inv_involutive q). by apply help. } intros p q Hpq. apply (mul_lt_mono_l _ _ q). rewrite mul_inv_r. apply (mul_lt_mono_r _ _ p). rewrite <-(assoc_L _), mul_inv_l. by rewrite mul_1_l, mul_1_r. Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)