proposition: Lemma Sumx_weird_lemma : forall n m l : nat, l = S (m + n) -> forall (f1 : forall i : nat, i < n -> IR) (f2 : forall i : nat, i < m -> IR) (f3 : forall i : nat, i < l -> IR), nat_less_n_fun f1 -> nat_less_n_fun f2 -> nat_less_n_fun f3 -> (forall (i : nat) Hi Hi', f1 i Hi [=] f3 i Hi') -> (forall (i : nat) Hi Hi', f2 i Hi [=] f3 (S (n + i)) Hi') -> (forall Hi, f3 n Hi [=] [0]) -> Sumx f1[+]Sumx f2 [=] Sumx f3.
proof: Proof. intros n m. induction m as [| m Hrecm]. intros l Hl. simpl in Hl; rewrite Hl; intros f1 f2 f3 Hf1 Hf2 Hf3 Hf1_f3 Hf2_f3 Hf3_f3. astepl (Sumx f1[+][0]). simpl in |- *; apply bin_op_wd_unfolded. apply Sumx_wd; intros; apply Hf1_f3. apply eq_symmetric_unfolded; apply Hf3_f3. set (l' := S m + n) in *. intros l Hl. rewrite Hl; intros f1 f2 f3 Hf1 Hf2 Hf3 Hf1_f3 Hf2_f3 Hf3_f3. apply eq_transitive_unfolded with (Sumx f1[+]Sumx (fun (i : nat) (Hi : i < m) => f2 i (Nat.lt_lt_succ_r _ _ Hi)) [+] f2 m (Nat.lt_succ_diag_r m)). simpl in |- *; algebra. astepr (Sumx (fun (i : nat) (Hi : i < l') => f3 i (Nat.lt_lt_succ_r _ _ Hi)) [+] f3 l' (Nat.lt_succ_diag_r l')). apply bin_op_wd_unfolded. apply Hrecm. unfold l' in |- *; auto. assumption. red in |- *; intros; apply Hf2; auto. red in |- *; intros; apply Hf3; auto. red in |- *; intros; apply Hf1_f3. red in |- *; intros; apply Hf2_f3. red in |- *; intros; apply Hf3_f3. unfold l' at 1 in |- *. cut (S (n + m) < S l'); [ intro | unfold l' in |- *; simpl in |- *; rewrite Nat.add_comm; auto ]. apply eq_transitive_unfolded with (f3 _ H). apply Hf2_f3. apply Hf3; simpl in |- *; auto with arith. Qed.
imports: CoRN.ftc.RefLemma Coq(Lia)