include "coa_defs.ma".
-theorem zero_le: \forall (P:COA). \forall (p:Type_of_COA P). le ? (zero P) p.
+coercion Type_of_COA. (* this should be generated by the following line *)
+coercion coa. (* this should be inside coa_defs.moo but it isn't *)
+
+theorem zero_le: \forall (P:COA). \forall (p:P). le ? (zero P) p.