proposition: Lemma clos_rt_idempotent : inclusion (R*)* R*.
proof: Proof. red. induction 1 as [x y H|x|x y z H IH H0 IH0]; auto with sets. apply rt_trans with y; auto with sets. Qed.
imports: Relation_Definitions Relation_Operators