proposition: Lemma part_tot_nat_fun_ch2 : forall n (f : forall i, i < n -> G) i, n <= i -> part_tot_nat_fun n f i [=] [0].
proof: Proof. intros n f i Hi. unfold part_tot_nat_fun in |- *. elim le_lt_dec; intro. simpl in |- *; algebra. exfalso; apply (Nat.le_ngt n i); auto. Qed.
imports: CoRN.algebra.CAbGroups Coq.Arith.Peano_dec Coq(Lia)