I have natural number list whose length is not zero ,but 1 mod length l is zero. It means length l is one because only 1 mod 1=0. Can i write this?

(length l) <> 0 ->

0= 1 mod (length l)->

(length l)=1.

Yes, this is provable (for any nat) as follows:

```
Require Import PeanoNat.
Lemma Test: forall (n : nat), n <> 0 -> 0 = 1 mod n -> n=1.
Proof.
intros n Hnz Hmod.
destruct n.
1: destruct Hnz; reflexivity.
Search (_ mod _ = 0).
pose proof Nat.mod_divides 1 (S n) Hnz as H.
destruct H as [H _].
specialize (H (eq_sym Hmod)).
destruct H.
symmetry in H.
Search(?a * ?b = 1).
apply Nat.mul_eq_1 in H.
tauto.
Qed.
```

Last updated: Jun 23 2024 at 23:01 UTC