proposition: Theorem inj_lt_inv: forall n m : nat, Z_of_nat n < Z_of_nat m -> (n < m)%nat.
proof: Proof. intros n m H; case (Nat.le_gt_cases m n); auto; intros H1; contradict H. apply Zle_not_lt; apply inj_le; auto. Qed.
imports: ZCAux List Root UList IGroup EGroup FGroup