proposition: Lemma Qcinv_nonneg : forall q, 0 <= / q <-> 0 <= q.
proof: Proof. intro q. unfold Qcle,Qcinv. do 2 rewrite Q2Qc_correct. split. intro. setoid_rewrite <- Qinv_involutive at 2. now apply Qinv_le_0_compat. now apply Qinv_le_0_compat. Qed.
imports: Qfield Qreduction Qcanon