proposition: Lemma Refinement_prop : Refinement -> forall i (Hi : i <= m) (HSi : (S i) <= m), {j : nat | {Hj : j <= n | {HSj : S j <= n | P _ Hj [<=] Q _ Hi | Q _ HSi [<=] P _ HSj}}}.
proof: Proof. intros H i Hi Hi'. elim H; clear H; intros f Hf. elim Hf; clear Hf; intros Hf0 Hf. elim Hf; clear Hf; intros Hfn Hfmon. intro Hf. cut {j : nat | f j <= i | S i <= f (S j)}. intro H. elim H; clear H; intros j Hj Hj'. exists j. cut (j < n). intro. cut (j <= n); [ intro Hj1 | auto with arith ]. exists Hj1. elim (Hf j Hj1); intros H' HPts. cut (S j <= n); [ intro Hj2 | apply H ]. elim (Hf (S j) Hj2); intros H'' HPts'. exists Hj2. eapply leEq_wdl. 2: eapply eq_transitive_unfolded. 2: apply eq_symmetric_unfolded; apply HPts. apply Partition_mon; assumption. apply prf1; auto. eapply leEq_wdr. 2: eapply eq_transitive_unfolded. 2: apply eq_symmetric_unfolded; apply HPts'. apply Partition_mon; assumption. apply prf1; auto. clear Hj' Hf Hf0. cut (i < f n). intro. cut (f j < f n); [ intro | apply Nat.le_lt_trans with i; auto ]. apply not_ge. intro; red in H1. apply (Nat.le_ngt (f j) (f n)); auto with arith. apply Hfmon. elim (le_lt_eq_dec _ _ H1); intro; auto. rewrite b0 in H0; elim (Nat.lt_irrefl (f j)); auto. rewrite <- Hfn in Hi'; auto. apply mon_fun_covers; auto. exists n; clear Hf Hfmon. rewrite Hfn; assumption. Qed.
imports: CoRN.ftc.Continuity Coq(Lia)