proposition: Lemma what_dL_does : forall p : Qpositive, dL p = Qpositive_mult p (Qpositive_inv (Qpositive_plus p One)).
proof: Proof. intros qp. unfold Qpositive_plus. functional induction (Qpositive_plus qp One). rewrite e;rewrite e0. rename q0 into q; rename e into H_eq_; rename e0 into H_eq_0. generalize (interp_non_zero qp). intros (p0, (q0, Hpq)). rewrite H_eq_ in Hpq. let f_local := eval compute in (f_equal (fst (B:=_)) Hpq) in let g_local := eval compute in (sym_eq (f_equal (fst (B:=_)) H_eq_0)) in generalize f_local g_local. let f_local := eval compute in (f_equal (snd (B:=_)) Hpq) in let g_local := eval compute in (sym_eq (f_equal (snd (B:=_)) H_eq_0)) in generalize f_local g_local. intros Hq Hq' Hp Hp'. subst. rewrite <- (mult_n_Sm (S q0) 0). repeat rewrite <- plus_n_Sm. rewrite <- mult_n_O. rewrite plus_O_n. rewrite Nat.mul_1_l. rewrite Nat.mul_1_r. unfold Qpositive_mult in |- *. rewrite H_eq_. set (P := Qpositive_i (Qpositive_c (S p0 + S q0) (S q0) (S (S p0 + S q0 + q0)))) in *. set (p' := fst P) in *. set (q' := snd P) in *. assert (H_P : Qpositive_i (Qpositive_c (S p0 + S q0) (S q0) (S (S p0 + S q0 + q0))) = (p', q')). replace (p', q') with P; trivial; unfold p', q' in |- *; apply pair_1. rewrite (inv_correct _ _ _ H_P). rewrite (Qpositive_c_unfold1 p0 q0 (S p0 + S q0 + q0)) in H_P. rewrite (construct_correct qp (S p0) (S q0) (S p0 + S q0 + q0) H_eq_ (Nat.le_add_r _ _)) in H_P. rewrite (Qpositive_i_nR qp _ _ H_eq_) in H_P. let f_local := eval cbv beta delta -[plus] in (sym_eq (f_equal (fst (B:=_)) H_P)) in let g_local := eval cbv beta delta -[plus] in (sym_eq (f_equal (snd (B:=_)) H_P)) in generalize f_local g_local. intros Hp' Hq'; rewrite Hp'; rewrite Hq'. clear H_eq_0 Hpq H_P Hp' Hq' P p' q'. rewrite <- (mult_n_Sm (S p0) q0). rewrite <- plus_n_Sm. rewrite (plus_Sn_m (S p0 * q0 + p0)). replace (S (S p0 * q0 + p0)) with (S q0 * S p0). rewrite Qpositive_c_dL. replace (S q0 * (S p0 + S q0) - S q0 * S p0) with (S q0 * S q0). apply f_equal with Qpositive. symmetry in |- *. rewrite (construct_correct4' (S q0 * S p0) (S q0 * S q0) (S p0) (S q0) (S p0 * q0 + p0 + S q0 * (S p0 + S q0)) (S p0 + S q0)). apply construct_correct. assumption. lia. rewrite <- mult_n_Sm. rewrite <- plus_n_Sm. auto with arith. rewrite <- mult_n_Sm. rewrite <- plus_n_Sm. auto with arith. auto with arith. auto with arith. rewrite Nat.mul_add_distr_l. rewrite <- (Nat.add_comm (S q0 * S p0 + S q0 * S q0)). apply Nat.le_add_r. apply le_n. rewrite (Nat.mul_comm (S q0) (S p0)). auto with arith. rewrite Nat.mul_add_distr_l. rewrite Nat.add_comm. rewrite Nat.add_sub; reflexivity. rewrite Nat.mul_add_distr_l. rewrite Nat.add_comm. repeat rewrite <- mult_n_Sm. rewrite <- plus_n_Sm. rewrite <- plus_n_Sm with (m := q0). generalize (S q0 * p0 + q0) (S q0 * q0 + q0); clear qp H_eq_; intros; lia. rewrite Nat.mul_comm. rewrite <- mult_n_Sm. rewrite <- plus_n_Sm; reflexivity. rewrite plus_n_Sm. apply le_n. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)