proposition: Lemma Q2Qc_eq_iff (q q' : Q) : Q2Qc q = Q2Qc q' <-> q == q'.
proof: Proof. split; intro H. - now injection H as [= H%Qred_eq_iff]. - apply Qc_is_canon. simpl. now rewrite H. Qed.
imports: Field QArith Znumtheory Eqdep_dec