proposition: Lemma image_monoid_prop_rev : forall y : M', in_part y image_monoid_hom -> exists x : M, Equal y (f x).
proof: Proof. simpl in |- *. intros y H'; try assumption. elim H'; intros x E; elim E; intros H'0 H'1; try exact H'0; clear E H'. exists x; try assumption. Qed.
imports: Monoid_util Parts2