proposition: Lemma Sumx_strext : forall n f g, nat_less_n_fun f -> nat_less_n_fun g -> Sumx _ f [#] Sumx _ g -> {N : nat | {HN : N < n | f N HN [#] g N HN}}.
proof: Proof. intro n; induction n as [| n Hrecn]. intros f g H H0 H1. elim (ap_irreflexive_unfolded _ _ H1). intros f g H H0 H1. simpl in H1. elim (bin_op_strext_unfolded _ _ _ _ _ _ H1); clear H1; intro H1. cut (nat_less_n_fun (fun (i : nat) (l : i < n) => f i (Nat.lt_lt_succ_r _ _ l))); [ intro H2 | red in |- *; intros; apply H; assumption ]. cut (nat_less_n_fun (fun (i : nat) (l : i < n) => g i (Nat.lt_lt_succ_r _ _ l))); [ intro H3 | red in |- *; intros; apply H0; assumption ]. elim (Hrecn _ _ H2 H3 H1); intros N HN. elim HN; clear HN; intros HN H'. exists N. exists (Nat.lt_lt_succ_r _ _ HN). eapply ap_wdl_unfolded. eapply ap_wdr_unfolded. apply H'. algebra. algebra. exists n. exists (Nat.lt_succ_diag_r n). eapply ap_wdl_unfolded. eapply ap_wdr_unfolded. apply H1. algebra. algebra. Qed.
imports: CoRN.algebra.CAbGroups Coq.Arith.Peano_dec Coq(Lia)