proposition: Lemma orsum_invariant5 r1 r2 r3: worder r1 -> worder r2 -> (order_sum2 r1 r2) \Is r3 -> (ordinal r1) +o (ordinal r2) = ordinal r3.
proof: Proof. move=> oa ob h. rewrite /osum2; apply: ordinal_o_isu1. apply: orsum2_wor. apply: (ordinal_o_wor (OS_ordinal oa)). apply: (ordinal_o_wor (OS_ordinal ob)). move: h (orsum2_wor oa ob); apply: worder_invariance. apply: orderIT h; apply: orsum_invariant4. apply: orderIS; apply: (ordinal_o_is oa). apply: orderIS; apply: (ordinal_o_is ob). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)