proposition: Lemma is_natural_sum_nat: is_natural_sum natural_sum.
proof: Proof. split. - apply: OS_natural_sum. - move => a b _ _;apply: natural_sumC. - apply: natural_sumA. - apply: natural_sum0. - move => a b c oa ob oc. by rewrite (natural_sumC c) (natural_sumC c); apply:ord_compare_nat_sum5. Abort. Section OsumS. Let S := doubleI_tdef2 (fun _ _ f => (osups (target f))). Lemma nsv_prop0: S =2o fun a b => osups (target (doubleI_restr2 S a b)). Proof. by apply:doubleI_tdef_rec2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)