proposition: Theorem order_lt: g_order pgroup < q * q.
proof: Proof. unfold g_order, pgroup, PGroup; simpl. rewrite <- (Z.abs_eq (q * q)); auto with zarith. rewrite <- (inj_Zabs_nat (q * q)); auto with zarith. rewrite <- mL_length; auto with zarith. apply inj_lt; apply isupport_length_strict with (0, 0). apply mL_ulist. apply mL_in; auto with zarith. intros a _; left; rewrite zpmult_0_l; auto with zarith. intros; discriminate. Qed.
imports: ZArith ZCAux Tactic Wf_nat NatAux UList ListAux FGroup EGroup PGroup IGroup