fact: Fixpoint eval_proof (p : proof) : { e : Z | 0 <= e} := match p with | Hyp e prf => exist _ e prf | Add p1 p2 => let (e1,p1) := eval_proof p1 in let (e2,p2) := eval_proof p2 in exist _ _ (add_le _ _ p1 p2) | Mul p1 p2 => let (e1,p1) := eval_proof p1 in let (e2,p2) := eval_proof p2 in exist _ _ (mul_le _ _ p1 p2) | Cst c => match Z_le_dec 0 c with | left prf => exist _ _ prf | _ => exist _ _ Z.le_0_1 end end.
imports: ZArithRing ZArith_base