Require Export pow.
Require Export Div2.
Require Export Even.
Lemma divltle2 : (c:nat)(lt O (div2 c))->(le (2) c).
Lemma div2_thm1 : (c:nat)(le (O) c)->(le (pred c) (plus (div2 c) (div2 c))).
Lemma div2_thm2 : (c:nat)(le (2) c)->(le (pred c) (plus (div2 c) (div2 c))).
Lemma div2_01 : (c:nat)(div2 c)=O->c=O\/c=(1).
Lemma div2_thm3 : (c:nat)(le (pred c) (plus (div2 c) (div2 c))).
Lemma div2_thm4 : (c:nat)(le (mult (2) (div2 c)) c).