proposition: Theorem in_mkLine: forall a n p, In p (mkLine a n) -> exists q, 0 <= q <= Z_of_nat n /\ p = (a, q).
proof: Proof. intros a n p; elim n; clear n. simpl; intros [H1 | H1]; exists 0; auto with zarith; case H1. simpl; intros n Rec [H1 | H1]; auto. exists (Z_of_nat (S n)); auto with zarith. case Rec; auto; intros q ((H2, H3), H4); exists q; repeat split. 1, 3: auto with zarith. change (q <= Z_of_nat (S n)). rewrite inj_S; auto with zarith. Qed.
imports: ZArith Znumtheory Tactic Wf_nat ListAux UList FGroup EGroup IGroup