proposition: Lemma mul_crealP (x y : creal) : creal_axiom (fun i => x i * y i).
proof: Proof. exists_big_modulus m F. move=> e i j e_gt0 hi hj. rewrite -[_ * _]subr0 -(subrr (x j * y i)) opprD opprK addrA. rewrite -mulrBl -addrA -mulrBr split_norm_add // !normrM. have /ler_wpmul2l /le_lt_trans-> // := uboundP y i. rewrite -ltr_pdivl_mulr ?ubound_gt0 ?cauchymodP //. by rewrite !pmulr_rgt0 ?invr_gt0 ?ubound_gt0 ?ltr0n. rewrite mulrC; have /ler_wpmul2l /le_lt_trans-> // := uboundP x j. rewrite -ltr_pdivl_mulr ?ubound_gt0 ?cauchymodP //. by rewrite !pmulr_rgt0 ?gtr0E ?ubound_gt0. by close. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrnum ssrint rat poly polydiv polyorder) mathcomp(perm matrix mxpoly polyXY binomial bigenough)