proposition: Lemma partition_join_Sum_lemma : Partition_Sum HfP (contin_imp_inc _ _ _ _ Hac') [+] Partition_Sum HfQ (contin_imp_inc _ _ _ _ Hcb') [=] Partition_Sum partition_join_Pts_in_partition (contin_imp_inc _ _ _ _ Hab').
proof: Proof. unfold Partition_Sum in |- *; apply Sumx_weird_lemma. auto with arith. Opaque partition_join. red in |- *; intros; apply mult_wd; algebra; apply cg_minus_wd; apply prf1; auto. red in |- *; intros; apply mult_wd; algebra; apply cg_minus_wd; apply prf1; auto. red in |- *; intros; apply mult_wd; try apply cg_minus_wd; try apply pfwdef; algebra. apply partition_join_Pts_wd; auto. apply prf1; auto. apply prf1; auto. Transparent partition_join. intros; apply mult_wd. apply pfwdef; apply eq_symmetric_unfolded; apply pjp_1. apply cg_minus_wd; simpl in |- *. unfold partition_join_fun in |- *; elim le_lt_dec; simpl in |- *; intro; [ apply prf1; auto | exfalso; apply Nat.le_ngt with n i; auto with arith ]. unfold partition_join_fun in |- *; elim le_lt_dec; simpl in |- *; intro; [ apply prf1; auto | exfalso; apply Nat.le_ngt with i n; auto with arith ]. intros; apply mult_wd. apply pfwdef. cut (i = S (n + i) - S n); [ intro | lia ]. generalize Hi; clear Hi; pattern i at 1 2 in |- *; rewrite H; intro. apply eq_symmetric_unfolded; apply pjp_3; auto with arith. apply cg_minus_wd; simpl in |- *. Opaque minus. unfold partition_join, partition_join_fun in |- *. elim le_lt_dec; simpl in |- *; intro. exfalso; apply Nat.nle_succ_diag_l with n; eapply Nat.le_trans. 2: apply a0. auto with arith. Transparent minus. apply prf1; transitivity (S (n + i) - n); auto with arith. Opaque minus. unfold partition_join, partition_join_fun in |- *. elim le_lt_dec; simpl in |- *; intro. exfalso; apply Nat.nle_succ_diag_l with n; eapply Nat.le_trans. 2: apply a0. auto with arith. Transparent minus. apply prf1; transitivity (n + i - n); auto with arith. intro; apply x_mult_zero. astepr (partition_join _ Hi[-]partition_join _ Hi). apply cg_minus_wd. algebra. unfold partition_join in |- *; simpl in |- *. apply eq_transitive_unfolded with c; unfold partition_join_fun in |- *; elim le_lt_dec; simpl in |- *. intro; apply finish. intro; exfalso; apply (Nat.lt_irrefl _ b0). intro; exfalso; apply (Nat.nle_succ_diag_l _ a0). intro; apply eq_symmetric_unfolded. apply eq_transitive_unfolded with (Q _ (Nat.le_0_l _)). apply prf1; auto with arith. apply start. Qed.
imports: CoRN.ftc.RefLemma Coq(Lia)