-lemma rtc_ism_inv_plus (n) (c1) (c2): ð\9d\90\8câ\9dªn,c1 + c2â\9d« →
- â\88\83â\88\83n1,n2. ð\9d\90\8câ\9dªn1,c1â\9d« & ð\9d\90\8câ\9dªn2,c2â\9d« & n1 + n2 = n.
+lemma rtc_ism_inv_plus (n) (c1) (c2): ð\9d\90\8câ\9d¨n,c1 + c2â\9d© →
+ â\88\83â\88\83n1,n2. ð\9d\90\8câ\9d¨n1,c1â\9d© & ð\9d\90\8câ\9d¨n2,c2â\9d© & n1 + n2 = n.