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