proposition: Lemma weaveSequencesSum : forall {R : ConstructiveReals} (fn gn : nat -> CRcarrier R) (n : nat), CRsum (fun k:nat => (weaveSequences (CRcarrier R) fn gn k)) n == CRsum fn (n / 2) + match n with | O => 0 | _ => CRsum gn (if Nat.even n then pred (n / 2) else n / 2) end.
proof: Proof. induction n. - unfold weaveSequences. simpl. rewrite CRplus_0_r. reflexivity. - simpl. rewrite IHn. clear IHn. destruct n. unfold weaveSequences. simpl. rewrite CRplus_0_r. reflexivity. assert (fst (Nat.divmod n 1 0 1) = n/2 )%nat. { reflexivity. } assert (fst (Nat.divmod n 1 0 0) = (1+n)/2 )%nat. { reflexivity. } unfold weaveSequences. simpl. destruct (Nat.even n) eqn:nEven. + destruct n. simpl. rewrite CRplus_assoc, (CRplus_comm (gn 0%nat)). rewrite <- CRplus_assoc. reflexivity. destruct (Nat.even n) eqn:snEven. rewrite evenSuccessor in nEven. rewrite snEven in nEven. inversion nEven. rewrite divModSucc. rewrite H. rewrite H0. pose proof (Nat.even_spec (S n)) as [H1 _]. destruct (H1 nEven). rewrite Nat.mul_comm in H2. rewrite H2. rewrite Nat.div_add. rewrite Nat.div_mul. simpl. do 2 rewrite CRplus_assoc. apply CRplus_morph. reflexivity. apply CRplus_comm. auto. auto. + destruct n. exfalso. inversion nEven. destruct (Nat.even n) eqn:snEven. rewrite divModSucc. rewrite H. rewrite H0. pose proof (Nat.odd_spec (S n)) as [H1 _]. destruct H1. unfold Nat.odd. rewrite nEven. trivial. rewrite Nat.mul_comm in H1. rewrite Nat.add_comm in H1. rewrite H1. rewrite Nat.div_add. assert ((1 + (1 + x * 2)) / 2 = (2 + x * 2) / 2)%nat. reflexivity. rewrite H2. rewrite Nat.div_add. simpl. do 2 rewrite CRplus_assoc. apply CRplus_morph. reflexivity. apply CRplus_morph. reflexivity. reflexivity. auto. auto. exfalso. rewrite <- nEven in snEven. rewrite evenSuccessor in snEven. destruct (Nat.even n); discriminate. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase