proposition: Lemma T1le_pmulr x a: T1nf a -> x != zero -> a <= a * x.
proof: Proof. move => na xnz. case az: (a==zero);first by rewrite (eqP az) T1mul0n. by rewrite - {1} (T1muln1 na) T1le_mul2l ? az // T1ge1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)