proposition: Lemma Qcinv_pos : forall q, 0 < /q <-> 0 < q.
proof: Proof. intro q. split; intro Hle. rewrite <- Qcinv_involutive. rewrite <- Qcmult_lt_r; try eassumption. rewrite Qcmult_0_l. rewrite Qcmult_inv_l. now compute. symmetry. now apply Qclt_not_eq. rewrite <- Qcmult_lt_r; try eassumption. rewrite Qcmult_0_l. rewrite Qcmult_inv_l. now compute. symmetry. now apply Qclt_not_eq. Qed.
imports: Qfield Qreduction Qcanon