proposition: Lemma RSR_auxR_lemmai : forall (i : nat) (Hi : 0 < i) (Hi' : i < m), RSR_auxR i = S (ProjT1 (RSR_h_g' (pred i) (lt_pred' _ _ Hi Hi'))).
proof: Proof. intros. unfold RSR_auxR in |- *. elim (le_lt_dec m i); intro; simpl in |- *. exfalso; apply Nat.le_ngt with m i; auto. elim (le_lt_dec i 0); intro; simpl in |- *. exfalso; apply Nat.lt_irrefl with 0; apply Nat.lt_le_trans with i; auto. set (x := ProjT1 (RSR_h_g' _ (lt_pred' _ _ b1 b0))) in *. set (y := ProjT1 (RSR_h_g' _ (lt_pred' _ _ Hi Hi'))) in *. cut (x = y). intro; auto with arith. assert (H := ProjT2 (RSR_h_g' _ (lt_pred' _ _ b1 b0))). assert (H0 := ProjT2 (RSR_h_g' _ (lt_pred' _ _ Hi Hi'))). elim H; clear H; intros Hx Hx'. elim H0; clear H0; intros Hy Hy'. apply RSR_h_inj with Hx Hy. eapply eq_transitive_unfolded. 2: apply Hy'. eapply eq_transitive_unfolded. apply eq_symmetric_unfolded; apply Hx'. apply RSR_g'_nlnf; reflexivity. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)