- partial commit of rt_transition ...

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / steps / rtc_plus.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_plus.ma b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_plus.ma
index 75a58b25f55b0abc1b7a8e4fc5280c139b0e927f..41f0e8a273e59ffc1875150bcb2311110cb1649c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_plus.ma
@@ -24,3 +24,13 @@ definition plus (r1:rtc) (r2:rtc): rtc ≝ match r1 with [
 
 interpretation "plus (rtc)"
    'plus r1 r2 = (plus r1 r2).
+
+(* Basic properties *********************************************************)
+
+lemma plus_OO_r: ∀r. r = 𝟘𝟘 + r.
+* normalize //
+qed.
+
+lemma plus_r_OO: ∀r. r = r + 𝟘𝟘.
+* normalize //
+qed.