proposition: Theorem zero_le : forall a, zero <= a.
proof: Proof. unfold le. destruct a; [left|right];repeat constructor. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List