proposition: Lemma Qpositive_c_1_1 : forall p q n' : nat, p - q <> 0 -> Qpositive_c p q (S n') = nR (Qpositive_c (p - q) q n').
proof: Proof. intros p q n' Hpq; simpl in |- *; elim (not_O_S _ Hpq); intros p' Hpq'; rewrite Hpq'; simpl in |- *; reflexivity. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)