proposition: Lemma RSR_auxP_lemma2 : forall (i : nat) (H : i <= n), {H' : RSR_auxP i <= _ | P i H[=]Separated_Refinement _ H'}.
proof: Proof. intros. unfold Separated_Refinement in |- *; simpl in |- *. unfold Separated_Refinement_fun in |- *; simpl in |- *. elim (le_lt_dec i 0); intro; simpl in |- *. cut (i = 0); [ intro | auto with arith ]. generalize H; clear a0 H; rewrite H0. rewrite RSR_auxP_lemma0. clear H0; intros. exists (Nat.le_0_l (pred (m + n))). elim le_lt_eq_dec; intro; simpl in |- *. elim (le_lt_dec 0 0); intro; simpl in |- *. apply start. exfalso; inversion b0. apply eq_transitive_unfolded with a. apply start. apply partition_length_zero with Hab. cut (m + n <= 1). intro. elim (plus_eq_one_imp_eq_zero _ _ H0); intro. rewrite <- a0; apply R. rewrite <- b1; apply P. generalize b0; clear b0. case (m + n). auto. intros. simpl in b0; rewrite <- b0; auto. elim (le_lt_eq_dec _ _ H); intro. cut (pred i < pred n); [ intro | apply Nat.lt_succ_lt_pred; rewrite Nat.lt_succ_pred with 0 i; auto ]. cut (RSR_auxP i <= pred (m + n)). intro; exists H1. elim le_lt_eq_dec; intro; simpl in |- *. elim (le_lt_dec (RSR_auxP i) 0); intro; simpl in |- *. cut (RSR_auxP i = 0); [ intro | auto with arith ]. rewrite <- RSR_auxP_lemma0 in H2. cut (RSR_auxP 0 < RSR_auxP i); [ intro | apply RSR_auxP_lemma1; assumption ]. exfalso; rewrite H2 in H3; apply (Nat.lt_irrefl _ H3). generalize b1 a1; clear b1 a1. rewrite (RSR_auxP_lemmai i b0 a0); intros. simpl in |- *. elim (ProjT2 (RSR_h_f' _ (lt_pred' i n b0 a0))); intros. eapply eq_transitive_unfolded. 2: eapply eq_transitive_unfolded. 2: apply p. unfold f' in |- *. apply prf1; symmetry; apply Nat.lt_succ_pred with 0; auto. apply RSR_h_nlnf; reflexivity. rewrite <- RSR_auxP_lemman in b1. cut (i = n). intro; exfalso; rewrite H2 in a0; apply (Nat.lt_irrefl _ a0). apply nat_mon_imp_inj with (h := RSR_auxP). apply RSR_auxP_lemma1. assumption. unfold RSR_auxP in |- *. elim (le_lt_dec i 0); intro; simpl in |- *. apply Nat.le_0_l. elim (le_lt_dec n i); intro; simpl in |- *. elim (Nat.lt_irrefl n); apply Nat.le_lt_trans with i; auto. apply plus_pred_pred_plus. elim (ProjT2 (RSR_h_f' _ (lt_pred' i n b1 b2))); intros. assumption. generalize H; clear H; rewrite b1; intro. rewrite RSR_auxP_lemman. exists (le_n (pred (m + n))). elim le_lt_eq_dec; intro; simpl in |- *. exfalso; apply (Nat.lt_irrefl _ a0). apply finish. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)