proposition: Lemma sum_diag_pascal2_0: sum_diag_pascal2 \0c = \1c.
proof: Proof. rewrite /sum_diag_pascal2/csumb Nint_cc00. set F := Lg _ _. have ha: domain F= singleton \0c by rewrite /F; aw. have hb: Vg F \0c = \1c. rewrite /F LgV; [by rewrite cdiff_nn (binom0 NS0) crem_12 |fprops]. have hc: cardinalp (Vg F \0c) by rewrite hb; apply: CS1. by rewrite (csum_trivial2 ha hc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)