proposition: Lemma mul_distr: right_distributive T1mul T1add.
proof: Proof. move => x y z; elim: y x z. by move => x z; rewrite T1muln0 !T1add0n. move => a _ n b Hb; case; first by move => z; rewrite ! T1mul0n. move => a' n' b'; case; first by rewrite T1muln0 ! T1addn0. move => a'' n'' b'' /=. case ha: (a'==zero); [rewrite (eqP ha) !andTb | rewrite !andFb ]. case hb: (a==zero); first rewrite (eqP hb). case hc: (a''==zero); last by move: hc; case a''. by rewrite (eqP hc) /= - !addnS mulnDr mulnS - !addnA (addnCA n) (addnCA n). case hc: (a'' == zero). rewrite (eqP hc) T1add0n add_simpl1 ? hb // T1ltn0. by rewrite T1lt0n hb /= hb Hb /=. simpl;case pa: (a < a''); first by rewrite /= hc. by case pb: (a'' < a); rewrite /= hb // Hb /= hc. case: (altP (a=P zero)) => hb. rewrite hb; case hc: (a''==zero). rewrite (eqP hc) /= ha T1ltnn /= mulnS mulnDr addnS ! addnA (addnC n'). by set X := (n' * n + n') %N;rewrite (addnAC (X + _)%N) (addnAC X). by rewrite T1ltn0 T1lt0n hc /negb /= ha hc add_le4 // hc. case hc: (a'' == zero). have h: a' < a' + a by apply: add_le4. rewrite (eqP hc) T1ltn0 T1lt0n hb /= ha /= h (T1lt_anti h) Hb //. by rewrite (negbTE hb) /= ha. rewrite /= ! T1lt_add2l. by case (T1ltgtP a a''); rewrite /=? ha ? hc ?(negbTE hb)//= Hb /= ha hc. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)