proposition: Lemma oprod2_comm2 a mu (x:= cnf_val a) (y := (oopow mu) *o x): cnfp_nz a -> \0o <o oexp a \0c -> ordinalp mu -> (cnf_degree a) +o mu = mu +o (cnf_degree a) -> oprod_comm x y.
proof: Proof. move=> anz vp om c1. have xp:= OS_cnf_valp anz. have ox := proj32_1 xp. have oe := (OS_cnf_degree anz). have oomu:= OS_oopow om. case: (ozero_dichot om) => muz. by rewrite /y muz oopow0 (oprod1l ox). move: (ord_rev_pred muz); set t:= _ -o _; move=> [ot tv]. have oot:= OS_oopow ot. have oot1:= OS_prod2 OS_omega oot. have ooe := OS_oopow oe. have oo := OS_omega. rewrite /oprod_comm - (oprodA oomu ox ox) (CNF_prod_pr4 anz anz vp). rewrite (oprodA oomu ooe ox) - (opow_sum oo om oe) - c1 (opow_sum oo oe om). rewrite /y /oopow tv (opow_sum oo OS1 ot) (opowx1 OS_omega). rewrite (oprodA ox oot1 ox) (oprodA ox oo oot) (CNF_prod_pr2 anz). by rewrite - (oprodA ooe oo oot). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)