proposition: Lemma generated_monoid_prop_rev : forall (M : MONOID) (A : part_set M) (y : M), (exists x : FM A, Equal y (FM_lift (inj_part A) x)) -> in_part y (generated_monoid A).
proof: Proof. intros M A y H'; try assumption. elim H'; intros x E; try exact E; clear H'. simpl in |- *; auto with algebra. exists x; split; [ idtac | try assumption ]. auto with algebra. Qed.
imports: Monoid_kernel Free_monoid