proposition: Lemma Bounded_M_dec: forall (M:Matrix), {Bounded_M M} + {~(Bounded_M M)}.
proof: Proof. intros ((a,b),(c,d)); unfold Bounded_M, fst, snd; case (Qlt_dec Zero (d+c)); intros; case (Qlt_dec Zero (d-c)); intros; case (Qlt_dec (d+c) Zero); intros; case (Qlt_dec (d-c) Zero); intros; tauto. Qed.
imports: Streams Streams_addenda Raxioms