proposition: Lemma Bounded_T_dec: forall (T:Tensor), {Bounded_T T} + {~(Bounded_T T)}.
proof: Proof. intros (((a,b),(c,d)),((e,f),(g,h))); unfold Bounded_T, fst, snd. case (Qlt_dec Zero (e+f+g+h)); case (Qlt_dec (e+f+g+h) Zero); intros; [ | | |tauto]; case (Qlt_dec Zero (e-f-g+h)); case (Qlt_dec (e-f-g+h) Zero); intros; [ | | |tauto| | | |tauto| | | |tauto]; case (Qlt_dec Zero (-e-f+g+h)); intros; case (Qlt_dec Zero (-e+f-g+h)); intros; case (Qlt_dec (-e-f+g+h) Zero); intros; case (Qlt_dec (-e+f-g+h) Zero); intros; tauto. Qed.
imports: Streams Streams_addenda Raxioms