proposition: Lemma RSR_auxR_lemma1 : forall i j : nat, i < j -> RSR_auxR i < RSR_auxR j.
proof: Proof. intros; unfold RSR_auxR in |- *. assert (X:=not_not_lt); assert (X':=plus_pred_pred_plus). assert (X'':=RSR_mn0); assert (X''':=RSR_nm0). elim (le_lt_dec i 0); intro. elim (le_lt_dec j 0); intros; simpl in |- *. apply Nat.le_lt_trans with i; try apply Nat.lt_le_trans with j; auto with arith. elim (le_lt_dec m j); intros; simpl in |- *. lia. apply Nat.lt_0_succ. elim (le_lt_dec m i); elim (le_lt_dec j 0); intros; simpl in |- *. elim (Nat.lt_irrefl 0); apply Nat.le_lt_trans with i; try apply Nat.lt_le_trans with j; auto with arith. elim (le_lt_dec m j); intro; simpl in |- *. apply Nat.add_lt_mono_l. apply Nat.add_lt_mono_l with m. repeat (rewrite Nat.add_comm; rewrite Nat.sub_add); auto. lia; auto; apply Nat.lt_trans with j; auto. elim (Nat.lt_irrefl 0); apply Nat.lt_trans with i; auto; apply Nat.lt_le_trans with j; auto. elim (le_lt_dec m j); intro; simpl in |- *. set (H0 := RSR_nm0) in *; set (H1 := RSR_mn0) in *; apply Nat.lt_le_trans with (S (pred m + pred n)). apply -> Nat.succ_lt_mono. apply (ProjT1 (ProjT2 (RSR_h_g' (pred i) (lt_pred' _ _ b0 b2)))). rewrite <- plus_Sn_m. rewrite Nat.lt_succ_pred with 0 m. 2: apply Nat.lt_trans with i; auto. replace (m + pred n) with (pred (m + n)). auto with arith. cut (S (pred (m + n)) = S (m + pred n)); auto. rewrite plus_n_Sm. rewrite Nat.lt_succ_pred with 0 n; auto with arith. apply Nat.lt_succ_pred with 0. apply Nat.lt_le_trans with m; auto with arith. apply Nat.lt_trans with i; auto. apply Nat.neq_0_lt_0. intro. apply Nat.lt_irrefl with 0. apply Nat.lt_trans with i; auto. rewrite RSR_nm0; auto. apply -> Nat.succ_lt_mono. cut (~ ~ ProjT1 (RSR_h_g' (pred i) (lt_pred' _ _ b0 b2)) < ProjT1 (RSR_h_g' (pred j) (lt_pred' _ _ b1 b3))); intro. apply not_not_lt; assumption. cut (ProjT1 (RSR_h_g' (pred j) (lt_pred' _ _ b1 b3)) <= ProjT1 (RSR_h_g' (pred i) (lt_pred' _ _ b0 b2))); intros. 2: apply not_lt; assumption. cut (h _ (ProjT1 (ProjT2 (RSR_h_g' (pred j) (lt_pred' _ _ b1 b3))))[<=] h _ (ProjT1 (ProjT2 (RSR_h_g' (pred i) (lt_pred' _ _ b0 b2))))). intro. 2: apply RSR_h_mon'; assumption. cut (g' (pred j) (lt_pred' _ _ b1 b3)[<=]g' (pred i) (lt_pred' _ _ b0 b2)). 2: apply leEq_wdl with (h _ (ProjT1 (ProjT2 (RSR_h_g' (pred j) (lt_pred' _ _ b1 b3))))). 2: apply leEq_wdr with (h _ (ProjT1 (ProjT2 (RSR_h_g' (pred i) (lt_pred' _ _ b0 b2))))). 2: assumption. 3: apply eq_symmetric_unfolded; exact (ProjT2 (ProjT2 (RSR_h_g' (pred j) (lt_pred' _ _ b1 b3)))). 2: apply eq_symmetric_unfolded; exact (ProjT2 (ProjT2 (RSR_h_g' (pred i) (lt_pred' _ _ b0 b2)))). clear H2 H1; intro. cut (g' _ (lt_pred' _ _ b0 b2)[<]g' _ (lt_pred' _ _ b1 b3)). 2: apply RSR_g'_mon. 2: apply lt_pred'; assumption. intro. exfalso. apply less_irreflexive_unfolded with (x := g' _ (lt_pred' _ _ b1 b3)). eapply leEq_less_trans; [ apply H1 | apply X0 ]. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)