proposition: Lemma osumA a b c: ordinalp a -> ordinalp b -> ordinalp c -> a +o (b +o c) = (a +o b) +o c.
proof: Proof. move => oa ob; move:c; apply:least_ordinal2' => d od H. rewrite (osum_rec_def oa (OS_sum2 ob od)) (osum_rec_def ob od). rewrite (osum_rec_def (OS_sum2 oa ob) od) {1} (osum_rec_def oa ob). set_extens t; case /setU2_P => h; apply /setU2_P. - left; fprops. - move /funI_P:h => [z /setU2_P ha ->]; case: ha. move => zb; left; apply /setU2_P;right; apply/funI_P;ex_tac. move => /funI_P [w wd ->]; rewrite (H _ wd); right; apply/funI_P; ex_tac. - case /setU2_P :h; first by left. move /funI_P => [z za ->]; right; apply /funI_P; exists z; fprops. - right; apply /funI_P; move/funI_P: h => [z zd ->]; rewrite - (H _ zd). exists (b +o z) => //;apply /setU2_P; right; apply /funI_P; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)