Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
branch: master
Fetching contributors…

Cannot retrieve contributors at this time

27 lines (23 sloc) 0.376 kb
Load "nat.tt";
Data Lt : (m,n:Nat)* where
ltO : (m:Nat)Lt O (S m)
| ltS : (m,n:Nat)(p:Lt m n)Lt (S m) (S n);
LtmSn : (m,n:Nat)(p:Lt m n)(Lt m (S n));
intros;
induction p;
intros;
refine ltO;
intros;
refine ltS;
fill p_IH;
Qed;
Ltmplus : (m,n,i:Nat)(p:Lt m n)(Lt m (plus n i));
intros;
induction p;
intros;
refine ltO;
intro m2 n1;
intros;
refine ltS;
fill p_IH;
Qed;
Jump to Line
Something went wrong with that request. Please try again.