proposition: Lemma Qpositive_c_dL : forall p q n' : nat, p < q -> Qpositive_c p q (S n') = dL (Qpositive_c p (q - p) n').
proof: Proof. intros p q n Hpq. generalize (lt_minus_eq_0 p q Hpq) (lt_minus_neq p q Hpq). intros Hpq0 Hqp. apply (Qpositive_c_1_0_1 _ _ n Hpq0 Hqp). Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)