proposition: Lemma nsvACA a b c d: ordinalp a -> ordinalp b -> ordinalp c -> ordinalp d -> S (S a b) (S c d) = S (S a c) (S b d).
proof: Proof. move => oa ob oc od. have h := (OS_nsv oa oc). rewrite (nsvC oa ob)- (nsvA ob oa (OS_nsv oc od)) (nsvA oa oc od). by rewrite (nsvC ob (OS_nsv h od)) - (nsvA h od ob) (nsvC od ob). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)