proposition: Lemma Qc_is_canon : forall q q' : Qc, q == q' -> q = q'.
proof: Proof. intros (q,hq) (q',hq') H. simpl in *. assert (H' := Qred_complete _ _ H). rewrite hq, hq' in H'. subst q'. f_equal. apply eq_proofs_unicity. intros. repeat decide equality. Qed.
imports: Field QArith Znumtheory Eqdep_dec