proposition: Lemma RSR_f'_ap_g' : forall (i j : nat) Hi Hj, f' i Hi[#]g' j Hj.
proof: Proof. intros. unfold f', g' in |- *; apply RSR_H'. apply Nat.lt_0_succ. apply Nat.lt_0_succ. apply pred_lt; assumption. apply pred_lt; assumption. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)