proposition: Lemma mul_addl : left_distributive mul add.
proof: Proof. elim/quotW=> x; elim/quotW=> y; elim/quotW=> z; apply/eqP. rewrite !piE /equivf /mulf /addf !numden_Ratio ?mulf_neq0 ?domP //; apply/eqP. rewrite !(mulrDr, mulrDl) (AC (3*(2*2)) (4*2*7*((1*3)*(6*5))))/=. by rewrite [X in _ + X](AC (3*(2*2)) (4*6*7*((1*3)*(2*5))))/=. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(ssrAC choice tuple bigop ssralg poly polydiv) mathcomp(generic_quotient)