proposition: Lemma partition_join_prf2 : forall (i : nat) H H', partition_join_fun i H [<=] partition_join_fun (S i) H'.
proof: Proof. intros. unfold partition_join_fun in |- *. elim (le_lt_dec i n); elim (le_lt_dec (S i) n); intros; simpl in |- *. apply prf2. cut (n = i); [ intro | apply Nat.le_antisymm; auto with arith ]. change (P i a0 [<=] Q (S i - S n) (partition_join_aux _ _ _ b0 H')) in |- *. generalize H' a0 b0; clear H' a0 b0. rewrite <- H0; intros. apply eq_imp_leEq. apply eq_transitive_unfolded with c. apply finish. apply eq_transitive_unfolded with (Q 0 (Nat.le_0_l _)). apply eq_symmetric_unfolded; apply start. apply prf1; auto with arith. exfalso; apply Nat.le_ngt with n i; auto with arith. cut (i - n = S (i - S n)); [ intro | lia ]. cut (S (i - S n) <= m); [ intro | lia ]. apply leEq_wdr with (Q _ H1). apply prf2. apply prf1; auto. Qed.
imports: CoRN.ftc.RefLemma Coq(Lia)