proposition: Lemma diameter_product_init_pure:forall alpha n H_diam, diameter(product_init_pure alpha n) H_diam= ub alpha n-lb alpha n.
proof: Proof. intros alpha n H_diam; unfold diameter; rewrite product_init_pure_ub; rewrite product_init_pure_lb; rewrite Qabs_eq_pos; trivial; apply Qlt_Qminus_Zero; apply lb_lt_ub_pointwise. Qed.
imports: QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier digits ub LNP_Digit homographic hcorrectness Refining_M Bounded_M Incl_M