proposition: Lemma foo : forall n, leb 0 n = true.
proof: Proof. intros. destruct n. - simpl. reflexivity. - simpl. reflexivity. Qed.
imports: Coq.Bool.Bool Coq.Arith.Arith Coq.Arith.EqNat Coq.omega.Omega Coq.Lists.List Coq.omega.Omega Maps