proposition: Lemma pi_add : {morph \pi : x y / addf x y >-> add x y}.
proof: Proof. move=> x y; unlock add; apply/eqmodP; rewrite /= equivfE /addf /=. rewrite !numden_Ratio ?mulf_neq0 ?domP // mulrDr mulrDl; apply/eqP. symmetry; rewrite (AC (2*2) (3*1*2*4)) (AC (2*2) (3*2*1*4))/=. by rewrite !equivf_l (ACl ((2*3)*(1*4))) (ACl ((2*3)*(4*1)))/=. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(ssrAC choice tuple bigop ssralg poly polydiv) mathcomp(generic_quotient)