proposition: Lemma Incl_T_dec_D: forall (T : Tensor) (D:Digit), {Incl_T T D} + {~(Incl_T T D)}.
proof: Proof. intros (((a,b),(c,d)),((e,f),(g,h))) D. unfold Incl_T. destruct (map_digits D) as ((dig1,dig2),(dig3,dig4)); unfold fst, snd. case (Bounded_T_dec (a, b, (c, d), (e, f, (g, h)))); intros; [|tauto]; case (Qle_dec ((e-f-g+h)*((e-f-g+h)*(dig2-dig1))) ((e-f-g+h)*((a-b-c+d)*(dig4-dig3)))); intros; [|tauto]; case (Qle_dec ((e-f-g+h)*((a-b-c+d)*(dig3+dig4))) ((e-f-g+h)*((e-f-g+h)*(dig1+dig2)))); intros; [|tauto]; case (Qle_dec ((-e-f+g+h)*((-e-f+g+h)*(dig2-dig1))) ((-e-f+g+h)*((-a-b+c+d)*(dig4-dig3)))); intros; [|tauto]; case (Qle_dec ((-e-f+g+h)*((-a-b+c+d)*(dig3+dig4))) ((-e-f+g+h)*((-e-f+g+h)*(dig1+dig2)))); intros; [|tauto]; case (Qle_dec ((-e+f-g+h)*((-e+f-g+h)*(dig2-dig1))) ((-e+f-g+h)*((-a+b-c+d)*(dig4-dig3)))); intros; [|tauto]; case (Qle_dec ((-e+f-g+h)*((-a+b-c+d)*(dig3+dig4))) ((-e+f-g+h)*((-e+f-g+h)*(dig1+dig2)))); intros; [|tauto]; case (Qle_dec ((e+f+g+h)*((e+f+g+h)*(dig2-dig1))) ((e+f+g+h)*((a+b+c+d)*(dig4-dig3)))); intros; [|tauto]; case (Qle_dec ((e+f+g+h)*((a+b+c+d)*(dig3+dig4))) ((e+f+g+h)*((e+f+g+h)*(dig1+dig2)))); intros; [|tauto]; left; split; trivial; repeat split; assumption. Qed.
imports: Streams Streams_addenda Raxioms