proposition: Lemma explicitation : forall (z z' : C) (M M' : PO), z = affixe M -> z' = affixe M' -> M' = g M -> z' = Cplus (Cmult a z) b.
proof: Proof. intros. rewrite H0; rewrite H1; rewrite g_def. rewrite affixe_transforme; rewrite <- H; rewrite f_def; auto. Qed.