proposition: Lemma T1lt_mul2r x y z: (y * x < z * x) -> (y < z).
proof: Proof. elim: x y z => // a Ha n b Hb. case => //; [ case => // | move => a' n' b'; case]. by rewrite ! (fun_if (fun z => z < zero)) ! T1ltn0 !if_same. move => a'' n'' b'' /=. case pa: (a'==zero). case pb: (a==zero). rewrite (eqP pa) !andbT (eq_sym zero a'') T1lt0n;case a'' => //=. by rewrite T1ltnn if_same if_simpl - ! mulnSr ltn_add2r ltn_mul2r /= => ->. by case a''; rewrite (eqP pa) // !andbF /= !T1ltnn ltnn ! eqxx; move /Hb. case pb: (a==zero). case pc: (a''==zero); rewrite ! andbT /= ?pa? T1ltn0 //. case (T1ltgtP a' a'') => //. by rewrite - ! mulnSr ltn_add2r ltn_mul2r eqn_add2r eqn_mul2r /=. rewrite ! andbF /= ltnn eqxx. case pc: (a' + a < a'' + a); first by rewrite (T1lt_add2r pc). by case pd: (a' + a == a'' + a) => // /Hb. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)