proposition: Lemma nsvC a b: ordinalp a -> ordinalp b -> (S a b) = (S b a).
proof: Proof. move => oa; move: a oa b. apply: least_ordinal2' => a oa ap. apply: least_ordinal2' => b ob bp. rewrite (nsv_rec oa ob) (nsv_rec ob oa); congr osups. set_extens t. move/doubleI_rgP; case => - [y yi ->]; apply /doubleI_rgP. right; ex_tac. left; ex_tac. move/doubleI_rgP;case => - [y yi ->]; apply /doubleI_rgP. by right; ex_tac; symmetry; apply: ap. by left; ex_tac; symmetry; apply: bp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)