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