proposition: Lemma weaveSequencesOdd : forall (X : Set) (fn gn : nat -> X) (n : nat), weaveSequences X fn gn (1 + n*2) = gn n.
proof: Proof. intros. unfold weaveSequences. destruct (Nat.even (1 + n * 2)) eqn:even. exfalso. rewrite evenSuccessor in even. assert (Nat.even (n * 2) = true). apply Nat.even_spec. exists n. rewrite Nat.mul_comm. reflexivity. rewrite H in even. discriminate. rewrite Nat.div_add. simpl. reflexivity. auto. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase