lemma isrt_inv_plus_O_dx: ∀n,c1,c2. 𝐑𝐓⦃n, c1 + c2⦄ → 𝐑𝐓⦃0, c2⦄ → 𝐑𝐓⦃n, c1⦄.
#n #c1 #c2 #H #H2
elim (isrt_inv_plus … H) -H #n1 #n2 #Hn1 #Hn2 #H destruct
lemma isrt_inv_plus_O_dx: ∀n,c1,c2. 𝐑𝐓⦃n, c1 + c2⦄ → 𝐑𝐓⦃0, c2⦄ → 𝐑𝐓⦃n, c1⦄.
#n #c1 #c2 #H #H2
elim (isrt_inv_plus … H) -H #n1 #n2 #Hn1 #Hn2 #H destruct