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