proposition: Lemma Qred_1_r : forall n, Qred (n#1) = n#1.
proof: Proof. intro n. unfold Qred. cut (Z.ggcd n 1 = (1, (n, 1)))%Z. intro H. now rewrite H. pose (Hggcd := Z.ggcd_correct_divisors n 1). clearbody Hggcd. assert (fst (Z.ggcd n 1) = 1%Z) as Hgcd. rewrite Z.ggcd_gcd. now apply Z.gcd_1_r. destruct (Z.ggcd n 1) as [d [a b]]. simpl in *. subst. f_equal. do 2 rewrite Zmult_1_l in Hggcd. now destruct Hggcd; subst. Qed.
imports: Qfield Qreduction Qcanon