proposition: Lemma oprod_comm_deg a b: \0o <o a -> \0o <o b -> odegree a = odegree b -> oprod_comm a b -> a +o b = b +o a.
proof: Proof. move => ap bp dab c. have Q u v: natp u -> natp v -> u +o v = v +o u. by move => aN bN;rewrite (osum2_2int aN bN) csumC (osum2_2int bN aN). case/(oprod2_comm (proj32_1 ap) (proj32_1 bp)):c. by move => az; case: (nesym (proj2 ap)). case; first by move => bz; case: (nesym (proj2 bp)). case. wlog: a b ap bp dab / (oprod2_comm_P4 a b). move => H; case => //. by move => h; apply: (H a b) => //; left. by move => h; symmetry;apply: (H b a ) => //; left. move => [c [e [n [m [cc cl oe [nN mN xv dd yv]]]]]] _. have oem := (OS_prod2 oe (OS_nat mN)). have oen := (OS_prod2 oe (OS_nat nN)). have fp: \0o <o oopow (e *o m) by apply: oopow_pos. move: dab; rewrite yv (odegree_prod fp ap) (odegree_opow oem). have ->: odegree a = e *o n. rewrite /odegree (Y_false (nesym (proj2 ap))) xv. by rewrite (proj43 (cnf_and_val_pb (proj1 cc))). rewrite - (oprodD (OS_nat mN) (OS_nat nN) oe) (Q m n mN nN). rewrite (oprodD (OS_nat nN) (OS_nat mN) oe). rewrite -{1} (osum0r oen); move / (osum2_simpl OS0 oem oen) => <-. by rewrite oopow0 (oprod1l (proj32_1 ap)). case. by move => [ /(oltP OS_omega) aN /(oltP OS_omega) bN]; rewrite Q. move => [e [n [m [oe nN mN]]]] => av bv. case: (oleT_el OS_omega oe) => ef; last first. by rewrite av bv;apply:Q; apply/(oltP OS_omega); apply: opow_2int1 => //; apply/(oltP OS_omega). move: (odegree_infinite ef) => enz. have np := (olt_leT olt_0omega ef). have H: forall k, natp k -> odegree (e ^o k) = (odegree e) *o k. apply: Nat_induction. by rewrite opowx0 oprod0r odegree_one. move => k kN Hrec. rewrite (succ_of_nat kN) (opow_succ oe (OS_nat kN)). rewrite (odegree_prod (opow_pos np (OS_nat kN)) np). by rewrite Hrec (oprod2_succ (OS_degree oe) (OS_nat kN)). move: dab; rewrite av bv (H _ nN) (H _ mN). by move/(oprod2_simpl (OS_nat nN) (OS_nat mN) enz) => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)