proposition: Lemma oleading_coef_prod1 x y: \0o <o x -> posnatp y -> oleading_coef (x *o y) =(oleading_coef x) *c y.
proof: Proof. move => xp kp. rewrite/oleading_coef. move:(the_cnf_p0_nz xp) => [sa sb]. move:(CNF_prod_pr1 sa kp); rewrite sb => ha. move: (cpred_pr (proj1 kp) (nesym(proj2(proj2 kp)))) => [qa qb]. move: (cnf_nck_prop3 sa qa); rewrite - qb => ax. move: (proj43 (cnf_and_val_pb ax)); rewrite - ha => ->. rewrite /cnf_nck/cnf_size Lgd/ocoef. have id: inc (cpred (domain (the_cnf x))) (domain (the_cnf x)). move: (cnf_size_nz sa)=> [qc qd]. by rewrite qd cpred_pr1; fprops; apply: Nsucc_i. by rewrite LgV ///cnf_c; Ytac0; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)