proposition: Lemma partialApplyWeaveEven : forall {R : ConstructiveReals} (X : Set) (fn gn : nat -> @PartialFunction R X) (n : nat) (x : X) (xD : Domain (fn n) x) (y : Domain (weaveSequences (PartialFunction X) fn gn (n*2)) x), partialApply (fn n) x xD == partialApply (weaveSequences (PartialFunction X) fn gn (n * 2)) x y.
proof: Proof. intros. unfold weaveSequences. unfold weaveSequences in y. destruct (Nat.even (n * 2)) eqn:des. remember ((n * 2) / 2)%nat as doubleN. rewrite Nat.div_mul in HeqdoubleN. subst doubleN. apply DomainProp. auto. exfalso. assert (Nat.even (n * 2) = true). apply Nat.even_spec. exists n. rewrite Nat.mul_comm. reflexivity. rewrite des in H. discriminate. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase