proposition: Lemma nonorigine_image_nonzero : forall (M : PO) (z : C), O <> M -> M = image z -> z <> zeroC :>C.
proof: Proof. intros. red in |- *; intros; apply H. rewrite H0; rewrite H1. symmetry in |- *; auto with geo. Qed.