proposition: Lemma Qpositive_c_equal_One : forall m n p : nat, m = n -> Qpositive_c m n p = One.
proof: Proof. intros p q [| n'] Hpq; [ apply Qpositive_c_0 | apply Qpositive_c_1_0_0; rewrite Hpq; rewrite Nat.sub_diag ]; reflexivity. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)