proposition: Lemma cprod_An1 a b f: ordinalp a -> ordinalp b -> cprodb (a +o b) f = cprodb a f *c cprodb b (fun z => f (a +o z)).
proof: Proof. move => oa ob. rewrite {1} /cprodb; set g := Lg (a +o b) f. have fgg: fgraph g by rewrite /g; fprops. have sab:= proj33 (osum_Mle0 oa ob). move: (is_partition_with_complement sab). have -> : a +o b = domain g by rewrite /g; aw. move=> pfa. rewrite (cprod_An pfa). rewrite /partition_with_complement Lgd//; symmetry; apply: cprod2_pr. set ff := fun l: Set => _. have ->: cprodb a f = ff C0. rewrite /ff /g; aw ;apply: cprodb_exten => s sf /=. by rewrite LgV//;apply: sab. suff: (cprodb b (fun z => f (a +o z))) = ff C1 by move => ->; apply doubleton_fam_canon. rewrite /ff /g;aw. have -> : cprodb ((a +o b) -s a)(Vg (Lg (a +o b) f)) = cprodb ((a +o b) -s a) f. apply: cprodb_exten => i /setC_P[ii _]; rewrite LgV//. symmetry;apply:cprod_Cn2; split. + move => t tb; apply/setC_P; rewrite (osum_rec_def oa ob);split. apply /setU2_P; right; apply/funI_P; ex_tac. by move=> /(oltP oa) h1; move:(oltNge h1(osum_Mle0 oa (Os_ordinal ob tb))). + move => u v uo vo su. move: (Os_ordinal ob uo) (Os_ordinal ob vo) => ou ov. exact (osum2_simpl ou ov oa su). + by rewrite (osum_rec_def oa ob); move => y /setC_P [/setU2_P] [] // /funI_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)