proposition: Lemma Qpositive_c_equal : forall m n p p' : nat, 0 < m -> 0 < n -> m + n <= p -> m + n <= p' -> Qpositive_c m n p = Qpositive_c m n p'.
proof: Proof. intros m n p. functional induction (Qpositive_c m n p) as [| | p q p' H_eq_1 | ]. intros p' _ _ Hpq. generalize (le_plus_O_l p q Hpq) (le_plus_O_r p q Hpq). intros Hp Hq. rewrite Hp. rewrite Hq. case p'; simpl in |- *; reflexivity. intros p' _ _ _ _. symmetry in |- *. apply Qpositive_c_equal_One. apply Nat.le_antisymm; apply minus_O_le; assumption. intros [| p'x] HpO HqO Hpq Hpq'. generalize (le_plus_O_r p q Hpq') (le_plus_O_l p q Hpq'). intros Hq Hp. apply False_ind;lia. rewrite Qpositive_c_1_0_1;auto. apply f_equal with Qpositive. rewrite (IHq p'x);try lia. unfold Qpositive_c at 2;fold Qpositive_c. rewrite e1. destruct (q - p);tauto. lia. intros [| p'x] HpO HqO Hpq Hpq'. generalize (le_plus_O_r p q Hpq') (le_plus_O_l p q Hpq'). intros Hq Hp. apply False_ind;lia. unfold Qpositive_c at 2;fold Qpositive_c. rewrite e0. rewrite (IHq p'x);try lia. reflexivity. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)