proposition: Lemma all_der_ident x i (f:= @id Set) (b:= fun x i => cnext (card_max x i)): ordinalp x -> ordinalp i -> all_der f b x i = x.
proof: Proof. set f1:= osum2 \0o. set b1 := fun x i => cnext (card_max (omax \0o x) i). have ha: forall x i, ordinalp x -> ordinalp i -> b1 x i = b x i. by rewrite /b /b1;move => x' i' ox oi; rewrite (omax_xy (ole0x ox)). move: (all_der_sum_aux OS0); rewrite -/b1 -/f1; move => [hb hc]. have sv: f1 =1o f by move => x' ox; rewrite /f1 (osum0l ox). have sb: all_der_bound f b. move => x' i' ox oi; rewrite - (ha _ _ ox oi). by move: (hc _ _ ox oi) => [ua ub uc ud]. move:OS0 => oz ox oi. rewrite - (all_der_unique hb hc sb sv ox oi) all_der_sum //. by rewrite oprod0l (osum0l ox). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)