proposition: Theorem canonicalp1 : forall a, ~ zeroP (A:=A) A0 eqA (n:=n) a -> canonical A0 eqA ltM (pX a (pO A n)).
proof: Proof. intros a H; split; simpl in |- *; auto. red in |- *; simpl in |- *; apply Relation_Operators_compat.d_one. Qed.
imports: Coq(Arith Compare_dec)