proposition: Lemma T1lt_mul2l x y z: x != zero -> T1nf z -> ((x *y < x *z) = (y < z)).
proof: Proof. case x => // a n b _; elim: y z. case;rewrite T1muln0 => // u v w //=; case a => //; case u => //. move => a' Ha n' b' Hb; case; first by rewrite T1muln0 ! T1ltn0. move => a'' n'' b'' nc. move/and3P:(nc) => [_ nb _] /=. case pa: (a==zero). case pb: (a'==zero). rewrite !andTb (eqP pb) (eqP pa); case a'' => //=. by rewrite ltn_simpl2 eqn_simpl2. rewrite !andTb (eqP pa) T1add0n. case pc: (a''==zero); first by rewrite /= pb (eqP pc) T1ltn0 pb. simpl;case pd:(a' < a'') => //; case pe:( a' == a'') => //. case pf:( n'< n'')%N => //; case pg:( n' == n'')%N => //. by move: (Hb _ nb); rewrite (eqP pa). simpl. case pb: (a'== zero). case pc: (a'' == zero). move: nc;rewrite (eqP pc) pb T1ltn0 T1nf_finite1=> /eqP ->. by rewrite /= !T1ltnn T1ltn0 eqxx ltn_simpl2 eqn_simpl2 if_same if_simpl. have: a < a + a'' by move: pc;rewrite -{1} (T1addn0 a) T1lt_add2l; case a''. by rewrite (eqP pb) /= => ->; move: pc; case a''. case pc: (a'' == zero). by rewrite (eqP pc) /= -{2 4} (T1addn0 a) T1lt_add2l T1eq_add2l !T1ltn0 pb. rewrite /= T1lt_add2l T1eq_add2l. case: (a' < a'') => //; case: (a' == a'') => //; case: (n' < n'')%N => //. by case: (n' == n'')%N => //; apply: Hb. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)