proposition: Lemma partition_join_mesh : Mesh partition_join [<=] Max (Mesh P) (Mesh Q).
proof: Proof. unfold Mesh at 1 in |- *. apply maxlist_leEq. apply length_Part_Mesh_List. apply Nat.lt_0_succ. intros x H. elim (Part_Mesh_List_lemma _ _ _ _ _ _ H); intros i Hi. elim Hi; clear Hi; intros Hi Hi'. elim Hi'; clear Hi'; intros Hi' Hx. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply Hx. unfold partition_join in |- *; simpl in |- *. unfold partition_join_fun in |- *. elim le_lt_dec; intro; simpl in |- *. elim le_lt_dec; intro; simpl in |- *. eapply leEq_transitive. apply Mesh_lemma. apply lft_leEq_Max. exfalso; apply Nat.le_ngt with i n; auto with arith. elim le_lt_dec; intro; simpl in |- *. cut (i = n); [ intro | apply Nat.le_antisymm; auto with arith ]. generalize a0 b0 Hi'; clear Hx Hi Hi' a0 b0. rewrite H0; intros. apply leEq_wdl with ZeroR. eapply leEq_transitive. 2: apply lft_leEq_Max. apply Mesh_nonneg. astepl (c[-]c). apply eq_symmetric_unfolded; apply cg_minus_wd. cut (forall H, Q (n - n) H [=] c); auto. cut (n - n = 0); [ intro | auto with arith ]. rewrite H1; intros; apply start. apply finish. cut (i - n = S (i - S n)); [ intro | lia ]. cut (forall H, Q (i - n) H[-]Q _ (partition_join_aux _ _ _ b1 Hi) [<=] Max (Mesh P) (Mesh Q)); auto. rewrite H0; intros; eapply leEq_transitive. apply Mesh_lemma. apply rht_leEq_Max. Qed.
imports: CoRN.ftc.RefLemma Coq(Lia)