proposition: Lemma cdiff_succ a b: cardinalp a -> cardinalp b -> (csucc a) -c (csucc b) = a -c b.
proof: Proof. move => ca cb. case :(cleT_el ca cb) => lea. by move:(cleSS lea) => leb; rewrite (cdiff_wrong leb)(cdiff_wrong lea). case /finite_or_infinite: cb => fb; last first. move:(cle_inf_inf fb (proj1 lea)) => /csucc_inf <-. by move/csucc_inf: fb <-. case /finite_or_infinite: ca => fa; last first. move/(finite_succP (proj31_1 lea)):(fb) => fsb. move /csucc_inf: (fa) => <-. by rewrite (cdiff_fin_infin fsb fa)(cdiff_fin_infin fb fa). move: fa fb => /NatP aN /NatP bN. rewrite (succ_of_nat aN) (succ_of_nat bN) /cdiff /osucc. move/olt_i: (oclt lea) => iba. move:(oclt lea) => [[ob oa sab] anb]. have aa:= (ordinal_irreflexive oa). set E := (a -s (b +s1 b)). have naE: ~inc a E by move /setC_P => [/aa]. have nbE: ~inc b E by move /setC_P => [_] /setU1_P; case; right. have -> : a -s b = E +s1 b. set_extens t. move/setC_P => [ta tb];case: (equal_or_not t b) => tc. by rewrite tc; fprops. by apply:setU1_r; apply: (setC_i ta);case/setU1_P. case/setU1_P. move/setC_P => [ta ntb];apply: (setC_i ta) => itb; case: ntb; fprops. move => ->; apply: (setC_i iba); apply:(ordinal_irreflexive ob). have -> : ((a +s1 a) -s (b +s1 b)) = E +s1 a. set_extens t. move/setC_P => [ta tb]; case/setU1_P: ta => ta. by apply:setU1_r;apply/setC_P. by rewrite ta; apply:setU1_1. case/setU1_P. move/setC_P => [ta tb]; apply:(setC_i _ tb); fprops. move ->; apply/setC_P; split => //; fprops => w. by move: (extensionality sab (ordinal_sub3 ob w)). by rewrite (csucc_pr naE) (csucc_pr nbE). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)