proposition: Lemma osum2_2int a b: natp a -> natp b -> a +o b = a +c b.
proof: Proof. move=> aN bN;move: b bN. have oa:= OS_nat aN. apply: Nat_induction; first by rewrite (Nsum0r aN) (osum0r oa). move=> n nN hrec. rewrite (csum_nS _ nN) (succ_of_nat nN) (succ_of_nat (NS_sum aN nN)). by rewrite - (osum2_succ oa (OS_cardinal (CS_nat nN))) hrec. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)