fact: Definition is_natural_sum (f: fterm2) := [/\ forall a b, ordinalp a -> ordinalp b -> ordinalp (f a b), forall a b, ordinalp a -> ordinalp b -> (f a b) = f b a, forall a b c, ordinalp a -> ordinalp b -> ordinalp c -> f a (f b c) = f (f a b) c, forall a, ordinalp a -> f a \0o = a & forall a b c, ordinalp a -> ordinalp b -> ordinalp c -> (f c a <=o f c b <-> a <=o b)].
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)