Changeset 2211 for src/ASM/Util.ma


Ignore:
Timestamp:
Jul 18, 2012, 3:57:09 PM (7 years ago)
Author:
boender
Message:
  • finished proof of sigma specification
  • added some stuff to Util, as usual
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r2149 r2211  
    17551755  cases (lt_to_not_zero … relevant)
    17561756qed.
     1757
     1758lemma ltb_false_to_not_lt: ∀p,q:ℕ.ltb p q = false → p ≮ q.
     1759  #p #q #H @leb_false_to_not_le @H
     1760qed.
     1761
     1762lemma ltb_true_to_lt: ∀p,q:ℕ.ltb p q = true → p < q.
     1763 #p #q #H @leb_true_to_le @H
     1764qed.
     1765 
     1766lemma plus_equals_zero: ∀x,y:ℕ.x + y = x → y = 0.
     1767 #x #y cases y
     1768 [ #_ @refl
     1769 | -y #y elim x
     1770   [ <plus_O_n / by /
     1771   | -x #x #Hind #H2 @Hind normalize in H2; @injective_S @H2
     1772   ]
     1773 ]
     1774qed.
Note: See TracChangeset for help on using the changeset viewer.