proposition: Lemma nsv_natsum: is_natural_sum S.
proof: Proof. split. - apply: OS_nsv. - apply: nsvC. - by move => a bc oa ob oc; apply: nsvA. - apply:nsv_n0. - move => a b c oa ob oc; split => h; last exact:(nsv_ler oc h). by case: (oleT_el oa ob)=> // /(nsv_ltr oc) /oltNge; case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)