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