proposition: Lemma point_fixe_gf : forall M : PO, g M = M -> f (affixe M) = affixe M.
proof: Proof. intros M; try assumption. repeat rewrite g_def; intros. pattern M at 2 in |- *. rewrite <- H. rewrite affixe_transforme; auto. Qed.