proposition: Lemma Bounded_T_nonzero: forall a b c d e f g h, Bounded_T (((a,b),(c,d)),((e,f),(g,h))) -> h<> Zero.
proof: Proof. intros a b c d e f g h [[H1 [H2 [H3 H4]]]|[H1 [H2 [H3 H4]]]] H5 ; unfold fst, snd in H1; unfold fst, snd in H2; unfold fst, snd in H3; unfold fst, snd in H4; generalize H1 H2 H3 H4; clear H1 H2 H3 H4; rewrite H5; unfold Qminus; repeat rewrite Qplus_zero_right; intros H1 H2 H3 H4; apply Qlt_irreflexive with Zero; [ stepr ((e + f + g)+(e + - f + - g)+(- e + - f + g)+(- e + f - g)) | stepl ((e + f + g)+(e + - f + - g)+(- e + - f + g)+(- e + f - g)) ]; auto; ring. Qed.
imports: digits Bounded_M Raxioms RIneq QArithSternBrocot(R_addenda) Fourier_solvable_ineqs