proposition: Theorem q_more_than_square: Mp < q * q.
proof: Proof. unfold Mp. assert (2 ^ p <= q * q); auto with zarith. rewrite <- e_order_eq_p. apply Z.le_trans with (g_order pgroup). apply Zdivide_le; auto with zarith. apply Zlt_le_weak; apply e_order_pos; auto with zarith. 2: apply e_order_divide_order. 2: apply Zlt_le_weak; apply order_lt. apply Z.lt_le_trans with 2; auto with zarith. replace 2 with (Z_of_nat (length ((1, 0)::w::nil))); auto. unfold g_order; apply inj_le. apply ulist_incl_length. apply ulist_cons; simpl; auto. unfold w; intros [H2 | H2]; try (case H2; fail); discriminate. intro a; simpl; intros [H1 | [H1 | H1]]; subst. assert (In (1, 0) (mL q)). apply mL_in; auto with zarith. apply isupport_is_in; auto. apply is_inv_true with (1, 0); simpl; auto. intros; apply zpmult_1_l; auto with zarith. intros; apply zpmult_1_r; auto with zarith. exact w_in_pgroup. case H1. Qed.
imports: ZArith ZCAux Tactic Wf_nat NatAux UList ListAux FGroup EGroup PGroup IGroup