(* Properties with composition **********************************************)
lemma after_basic_rc (m2,m1,n2,n1):
- m1 â\89¤ m2 â\86\92 m2 â\89¤ m1+n1 â\86\92 ð\9d\90\81â\9d´m2,n2â\9dµ â\8a\9a ð\9d\90\81â\9d´m1,n1â\9dµ â\89\98 ð\9d\90\81â\9d´m1,n2+n1â\9dµ.
+ m1 â\89¤ m2 â\86\92 m2 â\89¤ m1+n1 â\86\92 ð\9d\90\81â\9d¨m2,n2â\9d© â\8a\9a ð\9d\90\81â\9d¨m1,n1â\9d© â\89\98 ð\9d\90\81â\9d¨m1,n2+n1â\9d©.
#m2 elim m2 -m2
[ #m1 #n2 #n1 #Hm21 #_
<(le_n_O_to_eq … Hm21) -m1 //