proposition: Lemma semantic_modulus_h_S_product:forall n n' mu alpha (H_r:Is_refining_M mu) H_r', let smodu':=semantic_modulus_h (product mu (map_digits (hd alpha))) (tl alpha) H_r' in let smodu:=semantic_modulus_h mu alpha H_r in (0 < n)%nat -> n' = projT1 smodu' -> n = projT1 smodu -> n = S n'.
proof: Proof. destruct n; intros n' mu alpha H_r H_r' smodu' smodu Hn_pos Hn' Hn; [inversion Hn_pos |]. set (d:=(proj1_sig (projT2 smodu))); set (d':=(proj1_sig (projT2 smodu'))); assert (Hd:d=(proj1_sig (projT2 smodu))); trivial; assert (Hd':d'=(proj1_sig (projT2 smodu'))); trivial; destruct (proj2_sig (projT2 smodu)) as [H1 H3]; destruct (proj2_sig (projT2 smodu')) as [H1' H3']. rewrite_all <- Hd; rewrite_all <- Hd'; rewrite_all <- Hn; rewrite_all <- Hn'. apply eq_S. destruct (lt_eq_lt_dec n n') as [[Hnn'|Hnn']|Hnn']; trivial. generalize (H3' n d Hnn'); rewrite_all (product_init_folds mu alpha n); contradiction... generalize (lt_n_S _ _ Hnn'); intros Hnn'_S; generalize (H3 (S n') d' Hnn'_S); rewrite (product_init_folds mu alpha n'); contradiction... Qed.
imports: QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier digits ub LNP_Digit homographic hcorrectness Refining_M Bounded_M Incl_M