proposition: Lemma omega_monom_inj a b c d: natp a -> natp b -> natp c -> natp d -> omega0 *o a +o b = omega0 *o c +o d -> (a = c /\ b = d).
proof: Proof. move => aN bN cN dN eq1. have aux: forall u v, natp u -> natp v -> natp (omega0 *o u +o v) -> u = \0c. move => u v uN vN /(oltP OS_omega) h; ex_middle h1. have l1:= (oprod_Mle1 OS_omega (ord_ne0_pos (OS_nat uN) h1)). by case:(oleNgt (oleT l1 (osum_Mle0 (proj32 l1) (OS_nat vN)))). case: (czero_dichot (CS_nat aN))=> az. move: eq1; rewrite az oprod0r (osum0l (OS_nat bN)) => eq1. rewrite eq1 in bN. by rewrite eq1 (aux _ _ cN dN bN) oprod0r (osum0l (OS_nat dN)). case: (czero_dichot (CS_nat cN))=> cz. move: eq1; rewrite cz oprod0r (osum0l (OS_nat dN)) => eq1. case: (nesym (proj2 az));rewrite - eq1 in dN; exact:(aux _ _ aN bN dN). move:(the_cnf_omega_kj (conj aN az) bN) => [_ [_ e1 e2]]. move:(the_cnf_omega_kj (conj cN cz) dN) => [_ [_ e3 e4]]. by rewrite eq1 in e1 e2; rewrite e1 in e3; rewrite e2 in e4. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)