proposition: Theorem mkLine_ulist: forall a n, ulist (mkLine a n).
proof: Proof. intros a n; elim n; simpl; auto. intros n1 H; apply ulist_cons; auto. change (~ In (a, Z_of_nat (S n1)) (mkLine a n1)). rewrite inj_S; intros H1. case in_mkLine with (1 := H1); auto with zarith. intros x ((H2, H3), H4); injection H4. intros H5; subst; auto with zarith. Qed.
imports: ZArith Znumtheory Tactic Wf_nat ListAux UList FGroup EGroup IGroup