proposition: Lemma Separated_Refinement_lemma2 : forall (i : nat) (H : i <= pred (m + n)) (H' : S i <= pred (m + n)), Separated_Refinement_fun i H[<=]Separated_Refinement_fun (S i) H'.
proof: Proof. intros; unfold Separated_Refinement_fun in |- *; simpl in |- *. elim (le_lt_eq_dec _ _ H); elim (le_lt_eq_dec _ _ H'); intros; simpl in |- *. elim (le_lt_dec i 0); elim (le_lt_dec (S i) 0); intros; simpl in |- *. exfalso; inversion a2. apply RSR_h_PropAll with (P := fun x : IR => a[<=]x). red in |- *; intros. apply leEq_wdr with x; assumption. intros; unfold f' in |- *. astepl (P 0 (Nat.le_0_l _)). apply Partition_mon; apply Nat.le_0_l. intros; unfold g' in |- *. astepl (R 0 (Nat.le_0_l _)). apply Partition_mon; apply Nat.le_0_l. exfalso; inversion a2. apply less_leEq; apply RSR_h_mon; auto with arith. elim (le_lt_dec i 0); elim (le_lt_dec (S i) 0); intros; simpl in |- *. exfalso; inversion a1. assumption. exfalso; inversion a1. apply RSR_h_PropAll with (P := fun x : IR => x[<=]b). red in |- *; intros. apply leEq_wdl with x; assumption. intros; unfold f' in |- *. apply leEq_wdr with (P _ (le_n _)). apply Partition_mon; apply Nat.le_trans with (pred n); auto with arith. apply finish. intros; unfold g' in |- *. apply leEq_wdr with (R _ (le_n _)). apply Partition_mon; apply Nat.le_trans with (pred m); auto with arith. apply finish. exfalso; rewrite <- b0 in H'; apply (Nat.nle_succ_diag_l _ H'). apply leEq_reflexive. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)