proposition: Lemma Incl_M_dec_D: forall (M : Matrix) (D:Digit), {Incl_M M D} + {~(Incl_M M D)}.
proof: Proof. intros ((a,b),(c,d)) D; unfold Incl_M; destruct (map_digits D) as ((dig1,dig2),(dig3,dig4)); simpl; case (Bounded_M_dec (a,b,(c,d))); intros ; [| tauto]; case (Qle_dec ((d-c)*((d-c)*(dig2-dig1))) ((d-c)*((b-a)*(dig4-dig3)))); intros; [|tauto]; case (Qle_dec ((d-c)*((b-a)*(dig3+dig4))) ((d-c)*((d-c)*(dig1+dig2)))); intros; [|tauto]; case (Qle_dec ((d+c)*((c+d)*(dig2-dig1))) ((d+c)*((a+b)*(dig4-dig3)))); intros; [|tauto]; case (Qle_dec ((d+c)*((a+b)*(dig3+dig4))) ((d+c)*((c+d)*(dig1+dig2)))); intros; tauto. Qed.
imports: Streams Streams_addenda Raxioms