proposition: Lemma Qpositive_c_0 : forall p q n : nat, n = 0 -> Qpositive_c p q n = One.
proof: Proof. intros p q n. functional induction (Qpositive_c p q n); trivial || (intros; discriminate). Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)