proposition: Lemma Qcinv_opp_comm : forall q, / -q = - /q.
proof: Proof. intros q. unfold Qcinv,Qcopp. apply Qc_is_canon. repeat rewrite Q2Qc_correct. destruct q as [[[][]]]; red; reflexivity. Qed.
imports: Qfield Qreduction Qcanon