proposition: Lemma Qcinv_pos x : 0 < x → 0 < /x.
proof: Proof. intros. assert (0 ≠ x) by (by apply Qclt_not_eq). by rewrite (Qcmult_lt_mono_pos_r _ _ x), Qcmult_0_l, Qcmult_inv_l by done. Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)