-lemma fr2_minus_inv_cons_sn_lt (f1) (f2) (d) (h) (i):
- ❨d, h❩;f1 ▭ i ≘ f2 → i < d →
- ∃∃f. f1 ▭ i ≘ f & f2 = ❨d-i,h❩;f.
-#f1 #f2 #d #h #i #H elim (fr2_minus_inv_cons_sn … H) -H *
+lemma fr2_minus_inv_lcons_sn_lt (f1) (f2) (d) (h) (i):
+ ❨d, h❩◗f1 ▭ i ≘ f2 → i < d →
+ ∃∃f. f1 ▭ i ≘ f & f2 = ❨d-i,h❩◗f.
+#f1 #f2 #d #h #i #H elim (fr2_minus_inv_lcons_sn … H) -H *