proposition: Lemma EquiPartitionMesh : forall {R : ConstructiveReals} (a b : CRcarrier R) (n last : nat) (leab : a <= b), PartitionMesh (ipt_seq (IntervalEquiPartition a b last leab)) (S n) == (b-a) * CR_of_Q R (1 # Pos.of_nat (S last)).
proof: Proof. induction n. - intros. unfold PartitionMesh, IntervalEquiPartition, ipt_seq. setoid_replace (Z.of_nat 0 # Pos.of_nat (S last))%Q with 0%Q. 2: reflexivity. rewrite CRmult_0_r, CRplus_0_r. unfold CRminus. rewrite CRplus_assoc, <- (CRplus_comm (-a)), <- CRplus_assoc. rewrite CRplus_opp_r, CRplus_0_l. rewrite CRmax_left. reflexivity. rewrite <- (CRmult_0_r (b-a)). apply CRmult_le_compat_l. rewrite <- (CRplus_opp_r a). apply CRplus_le_compat. exact leab. apply CRle_refl. apply CR_of_Q_le. discriminate. - intros. specialize (IHn last leab). unfold IntervalEquiPartition, ipt_seq. transitivity (CRmax ((a + (b - a) * CR_of_Q R (Z.of_nat (2+n) # Pos.of_nat (S last))) - (a + (b - a) * CR_of_Q R (Z.of_nat (1+n) # Pos.of_nat (S last)))) (PartitionMesh (ipt_seq (IntervalEquiPartition a b last leab)) (S n))). reflexivity. rewrite IHn. clear IHn. setoid_replace (a + (b - a) * CR_of_Q R (Z.of_nat (2 + n) # Pos.of_nat (S last)) - (a + (b - a) * CR_of_Q R (Z.of_nat (1 + n) # Pos.of_nat (S last)))) with ((b - a) * CR_of_Q R (1 # Pos.of_nat (S last))). rewrite CRmax_left. reflexivity. apply CRle_refl. rewrite CRplus_comm. unfold CRminus. rewrite CRopp_plus_distr, CRplus_assoc. rewrite <- (CRplus_assoc a), CRplus_opp_r, CRplus_0_l. rewrite CRopp_mult_distr_r, <- CRmult_plus_distr_l. apply CRmult_morph. reflexivity. rewrite <- CR_of_Q_opp, <- CR_of_Q_plus. apply CR_of_Q_morph. rewrite Qinv_minus_distr. unfold Qeq, Qnum, Qden. apply f_equal2. 2: reflexivity. simpl (2+n)%nat. rewrite (Nat2Z.inj_succ (S n)). unfold Z.succ. simpl (1+n)%nat. ring. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont