proposition: Theorem mkLine_in: forall a n p, 0 <= p <= Z_of_nat n -> (In (a, p) (mkLine a n)).
proof: Proof. intros a n; elim n. simpl; auto with zarith. intros p (H1, H2); replace p with 0; auto with zarith. intros n1 Rec p (H1, H2). case (Zle_lt_or_eq p (Z_of_nat (S n1))); auto with zarith. rewrite inj_S in H2; auto with zarith. rewrite inj_S; auto with zarith. intros H3; right; apply Rec; auto with zarith. intros H3; subst; simpl; auto. Qed.
imports: ZArith Znumtheory Tactic Wf_nat ListAux UList FGroup EGroup IGroup