proposition: Lemma nsvA a b c: ordinalp a -> ordinalp b -> ordinalp c -> S a (S b c) = S (S a b) c.
proof: Proof. move => oa ob oc; move: a oa c oc b ob. apply: least_ordinal2 => a oa ap. apply: least_ordinal2 => c oc cp. apply: least_ordinal2 => b ob bp. apply: oleA. apply: (nsv_le_prop oa (OS_nsv ob oc) (OS_nsv (OS_nsv oa ob) oc)). move => z za;rewrite (ap _ za _ oc _ ob). by apply:(nsv_ltl (nsv_ltl _ ob) oc). move => z /(nsv_lt_prop ob oc); case; move => [x lt1 lt2]. apply: (ole_ltT (nsv_ler oa lt2)). by rewrite (bp _ lt1); apply: (nsv_ltl (nsv_ltr oa lt1) oc). move: (nsv_ler oa lt2);rewrite (cp _ lt1 b ob) => ha. apply: (ole_ltT ha); apply: (nsv_ltr (OS_nsv oa ob) lt1). apply: (nsv_le_prop (OS_nsv oa ob) oc (OS_nsv oa (OS_nsv ob oc))). move => z /(nsv_lt_prop oa ob); case; move => [x lt1 lt2]. rewrite (nsvC (proj31 lt2) oc) (nsvC oc (proj31 lt2)). apply: (ole_ltT (nsv_lel lt2 oc)). rewrite - (ap _ lt1 _ oc _ ob); exact: (nsv_ltl lt1 (OS_nsv ob oc)). apply:(ole_ltT (nsv_lel lt2 oc)). by rewrite - (bp _ lt1); apply: (nsv_ltr oa (nsv_ltl lt1 oc)). by move => x lxc; rewrite - (cp _ lxc b ob); apply:(nsv_ltr oa (nsv_ltr ob _)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)