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