proposition: Lemma ltmc_add2r m m1 m2 : ((m + m1)%MM < (m + m2)%MM)%O = (m1 < m2)%O.
proof: Proof. case: (ltngtP (mdeg m1) (mdeg m2)) => [lt|lt|]. + by rewrite !lt_mdeg_ltmc // !mdegD ltn_add2l. + rewrite !ltNge !le_eqVlt !lt_mdeg_ltmc ?orbT //. by rewrite !mdegD ltn_add2l. move=> eq; have eqD: mdeg (m + m1) = mdeg (m + m2). by rewrite !mdegD (rwP eqP) eqn_add2l eq. apply/ltmcP/ltmcP => // {eq eqD} -[i eq lt]; exists i. + by move=> j /eq /eqP; rewrite !mnmDE (rwP eqP) eqn_add2l. + by move: lt; rewrite !mnmDE ltn_add2l. + by move=> j /eq /eqP; rewrite !mnmDE (rwP eqP) eqn_add2l. + by rewrite !mnmDE ltn_add2l. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(order fingroup perm ssralg zmodp poly ssrint) mathcomp(matrix vector) mathcomp(bigenough) ssrcomplements freeg