proposition: Lemma even_partition_Mesh : forall m Hm a b (Hab : a [<=] b), Mesh (Even_Partition Hab m Hm) [=] (b[-]a[/] _[//]nring_ap_zero' _ _ Hm).
proof: Proof. simple induction m. intros; exfalso; apply Hm; auto. intros. unfold Mesh in |- *. elim (le_lt_dec n 0); intro. cut (0 = n); [ intro | auto with arith ]. generalize Hm; clear H a0 Hm. rewrite <- H0; intros. simpl in |- *. rational. apply eq_transitive_unfolded with (Max (a[+]nring (S n) [*] (b[-]a[/] _[//]nring_ap_zero' _ _ Hm) [-] (a[+]nring n[*] (b[-]a[/] _[//]nring_ap_zero' _ _ Hm))) (maxlist (Part_Mesh_List (Partition_Dom (Even_Partition Hab _ Hm))))). cut (n = S (pred n)); [ intro | symmetry; apply Nat.lt_succ_pred with 0; auto ]. generalize Hm; rewrite H0; clear Hm; intro. simpl in |- *; algebra. eapply eq_transitive_unfolded. apply Max_comm. simpl in |- *. eapply eq_transitive_unfolded. apply leEq_imp_Max_is_rht. 2: rational. apply eq_imp_leEq. rstepr (b[-]a[/] nring n[+][1][//]nring_ap_zero' _ _ Hm). apply eq_transitive_unfolded with (Mesh (Partition_Dom (Even_Partition Hab _ Hm))). simpl in |- *; algebra. cut (0 <> n); intro. eapply eq_transitive_unfolded. apply Mesh_wd' with (Q := Even_Partition (part_pred_lemma _ _ Hab (S n) (Even_Partition Hab _ Hm) n (Nat.le_succ_diag_r n)) _ H0). intros; simpl in |- *; rational. eapply eq_transitive_unfolded. apply H. simpl in |- *; rational. apply (Nat.neq_0_lt_0 n); auto. Qed.
imports: CoRN.ftc.Continuity Coq(Lia)