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