proposition: Lemma denom_nonvanishing_T_Bounded_T: forall xi,(forall r1 r2,(-1 <= r1 <= 1)%R -> (-1 <= r2 <= 1)%R -> denom_nonvanishing_T xi r1 r2) -> Bounded_T xi.
proof: Proof. intros (((a,b),(c,d)),((e,f),(g,h))) H_denom. unfold denom_nonvanishing_T in H_denom; simpl in H_denom. assert (H_denomr1m:forall r1,(-1<=r1<=1)%R -> denom_nonvanishing_M (((-a+b),(-c+d)),((-e+f),(-g+h))) r1); [intros r1 Hr1; unfold denom_nonvanishing_M, fst, snd; realify_Q; stepl (e*r1*(-1)+f*r1+g*(-1)+h)%R; [|ring]; apply (H_denom r1 (-1)%R Hr1 min_one_is_in_base_interval)|]. assert (H_denomr1:forall r1,(-1<=r1<=1)%R -> denom_nonvanishing_M (((a+b),(c+d)),((e+f),(g+h))) r1); [intros r1 Hr1; unfold denom_nonvanishing_M, fst, snd; realify_Q; stepl (e*r1*1+f*r1+g*1+h)%R; [|ring]; apply (H_denom r1 (1)%R Hr1 one_is_in_base_interval)|]. assert (H_denomr2:forall r2,(-1<=r2<=1)%R -> denom_nonvanishing_M (((a+c),(b+d)),((e+g),(f+h))) r2); [intros r2 Hr2; unfold denom_nonvanishing_M, fst, snd; realify_Q; stepl (e*1*r2+f*1+g*r2+h)%R; [|ring]; apply (H_denom (1)%R r2 one_is_in_base_interval Hr2)|]. assert (H_denomr2m:forall r2,(-1<=r2<=1)%R -> denom_nonvanishing_M (((-a+c),(-b+d)),((-e+g),(-f+h))) r2); [intros r2 Hr2; unfold denom_nonvanishing_M, fst, snd; realify_Q; stepl (e*(-1)*r2+f*(-1)+g*r2+h)%R; [|ring]; apply (H_denom (-1)%R r2 min_one_is_in_base_interval Hr2)|]. assert (Hb1:=denom_nonvanishing_M_Bounded_M _ H_denomr1). assert (Hb1m:=denom_nonvanishing_M_Bounded_M _ H_denomr1m). assert (Hb2:=denom_nonvanishing_M_Bounded_M _ H_denomr2). assert (Hb2m:=denom_nonvanishing_M_Bounded_M _ H_denomr2m). assert (Hgh:=Bounded_M_nonzero _ _ _ _ Hb1). assert (Hghm:=Bounded_M_nonzero _ _ _ _ Hb1m). assert (Hfh:=Bounded_M_nonzero _ _ _ _ Hb2). assert (Hfhm:=Bounded_M_nonzero _ _ _ _ Hb2m). assert (H_efgh1:e-f-g+h<>Zero); [apply Q_to_R_Qneq; realify_Q_goal; stepl (e*(-1)*(-1)+f*(-1)+g*(-1)+h)%R; [|ring]; apply (H_denom (-1)%R (-1)%R min_one_is_in_base_interval min_one_is_in_base_interval)|]. assert (H_efgh2:-e-f+g+h<>Zero); [apply Q_to_R_Qneq; realify_Q_goal; stepl (e*(-1)*(1)+f*(-1)+g*(1)+h)%R; [|ring]; apply (H_denom (-1)%R (1)%R min_one_is_in_base_interval one_is_in_base_interval)|]. assert (H_efgh3:-e+f-g+h<>Zero); [apply Q_to_R_Qneq; realify_Q_goal; stepl (e*(1)*(-1)+f*(1)+g*(-1)+h)%R; [|ring]; apply (H_denom (1)%R (-1)%R one_is_in_base_interval min_one_is_in_base_interval)|]. assert (H_efgh4:e+f+g+h<>Zero); [apply Q_to_R_Qneq; realify_Q_goal; stepl (e*(1)*(1)+f*(1)+g*(1)+h)%R; [|ring]; apply (H_denom (1)%R (1)%R one_is_in_base_interval one_is_in_base_interval)|]. assert (Hh: h<>Zero); [apply Q_to_R_Qneq; realify_Q_goal; stepl (e*0*0+f*0+g*0+h)%R; [|ring]; apply H_denom; split; fourier.Fourier.fourier|]. unfold Incl_T, Bounded_T, map_digits, fst, snd. destruct (not_Qeq_inf _ _ Hgh) as [Hgh_sg|Hgh_sg]. right. assert (H_goal1:e+f+g+h<Zero); [ generalize (Bounded_M_neg _ _ _ _ (1)%R Hb1 Hgh_sg one_is_in_base_interval); rationalify_R_goal; intros H_; generalize (Q_to_R_Qlt _ _ H_); clear H_; intros H; ring_exact_Q H|]. assert (H_goal2:-e-f+g+h<Zero); [ generalize (Bounded_M_neg _ _ _ _ (-1)%R Hb1 Hgh_sg min_one_is_in_base_interval); rationalify_R_goal; intros H_; generalize (Q_to_R_Qlt _ _ H_); clear H_; intros H; ring_exact_Q H|]. assert (H_goal3:e-f-g+h<Zero). destruct (not_Qeq_inf _ _ H_efgh1) as [H_sg|H_sg]; trivial; assert (H_eg:Zero<e-g); [ apply Qlt_Qmult_cancel_l with (Qone+Qone); auto; stepl Zero; auto; stepr ((e-f-g+h)-(-e-f+g+h)); try ring; apply Qlt_Qminus_Zero; apply Qlt_transitive with Zero; trivial|]; contradiction (H_denomr2m ((-f+h)/(e-g))); simpl. split; rationalify_R; [ apply Qmult_pos_Qle_Qdiv; trivial; apply Qle_Zero_Qminus; stepr (e - f - g + h);[|ring] | apply Qmult_pos_Qdiv_Qle; trivial; apply Qle_Zero_Qminus_neg; stepl (-e - f + g + h); [|ring]]; auto. rationalify_R_goal; apply Q_to_Req; field; auto. repeat split; trivial. destruct (not_Qeq_inf _ _ H_efgh3) as [H_sg|H_sg]; trivial; assert (H_eg:Zero<f-e); [ apply Qlt_Qmult_cancel_l with (Qone+Qone); auto; stepl Zero; auto; stepr ((-e+f-g+h)-(e-f-g+h)); try ring; apply Qlt_Qminus_Zero; apply Qlt_transitive with Zero; trivial|]. contradiction (H_denomr1m ((g-h)/(f-e))); simpl. split; rationalify_R; [ apply Qmult_pos_Qle_Qdiv; trivial; apply Qle_Zero_Qminus_neg; stepl (e - f - g + h);[|ring] | apply Qmult_pos_Qdiv_Qle; trivial; apply Qle_Zero_Qminus; stepr (-e + f - g + h); [|ring]]; auto. rationalify_R_goal; apply Q_to_Req; field; auto. left. assert (H_goal1:Zero<e+f+g+h); [ generalize (Bounded_M_pos _ _ _ _ (1)%R Hb1 Hgh_sg one_is_in_base_interval); rationalify_R_goal; intros H_; generalize (Q_to_R_Qlt _ _ H_); clear H_; intros H; ring_exact_Q H|]. assert (H_goal2:Zero< -e-f+g+h); [ generalize (Bounded_M_pos _ _ _ _ (-1)%R Hb1 Hgh_sg min_one_is_in_base_interval); rationalify_R_goal; intros H_; generalize (Q_to_R_Qlt _ _ H_); clear H_; intros H; ring_exact_Q H|]. assert (H_goal3:Zero<e-f-g+h). destruct (not_Qeq_inf _ _ H_efgh1) as [H_sg|H_sg]; trivial. assert (H_eg:e-g<Zero); [ apply Qlt_Qmult_cancel_l with (Qone+Qone); auto; stepr Zero; auto; stepl ((e-f-g+h)-(-e-f+g+h)); try ring; apply Qlt_Qminus_Zero_neg; apply Qlt_transitive with Zero; trivial|]; contradiction (H_denomr2m ((-f+h)/(e-g))); simpl. split; rationalify_R; [ apply Qmult_neg_Qle_Qdiv; trivial; apply Qle_Zero_Qminus_neg; stepl (e - f - g + h);[|ring] |apply Qmult_neg_Qdiv_Qle; trivial; apply Qle_Zero_Qminus; stepr (-e - f + g + h); [|ring]]; auto. rationalify_R_goal; apply Q_to_Req; field; auto. repeat split; trivial. destruct (not_Qeq_inf _ _ H_efgh3) as [H_sg|H_sg]; trivial; assert (H_eg:f-e<Zero); [ apply Qlt_Qmult_cancel_l with (Qone+Qone); auto; stepr Zero; auto; stepl ((-e+f-g+h)-(e-f-g+h)); try ring; apply Qlt_Qminus_Zero_neg; apply Qlt_transitive with Zero; trivial |]. contradiction (H_denomr1m ((g-h)/(f-e))); simpl. split; rationalify_R; [ apply Qmult_neg_Qle_Qdiv; trivial; apply Qle_Zero_Qminus; stepr (e - f - g + h);[|ring] | apply Qmult_neg_Qdiv_Qle; trivial; apply Qle_Zero_Qminus_neg; stepl (-e + f - g + h); [|ring]]; auto. rationalify_R_goal; apply Q_to_Req; field; auto. Qed.
imports: digits Bounded_M Raxioms RIneq QArithSternBrocot(R_addenda) Fourier_solvable_ineqs