fact: Fixpoint ez2z (e:ExprZ) : Z := match e with | EZadd e1 e2 => ((ez2z e1)+(ez2z e2))%Z | EZsub e1 e2 => ((ez2z e1)-(ez2z e2))%Z | EZmul e1 e2 => ((ez2z e1)*(ez2z e2))%Z | EZmax e1 e2 => Z.max (ez2z e1) (ez2z e2) | EZopp e => (-(ez2z e))%Z | EZofI e => i2z (ei2i e) | EZraw z => z end.
imports: BinInt