mod lt possibly missing

Stream: mathlib4

[Matthew Pocock]

I hope mathlib4 is the right place to post this. I needed this auxiliary theorem:

theorem mod_one_gt_zero {n: Nat} : n%2=1 → 0 < n := by
    induction n
    simp
    simp

There's probably a neater way to write it. I couldn't find something in the standard library that did this job. Is it actually missing, or did I miss it? I needed it for mod 2, but I guess it generalises to any base, and could be a simplification rule. In general, I guess it is something like n%a \ne 0 -> 0 < n or perhaps n%a \ne 0 -> n \ne 0 maybe, but I specifically needed it to prove a 0<n bound.

[Yaël Dillies]

docs#Odd.pos

[Yaël Dillies]

You could also do λ h ↦ pos_iff_ne_zero.2 $ by rintro rfl; simpa using h. This generalizes to any base.

[Matthew Pocock]

Yaël Dillies said:

docs#Odd.pos

Thanks. To get that to behave I needed:

        simp only [← Nat.odd_iff] at nh -- rewrite the assumption `n%2=1` to `Odd n`
        use Odd.pos nh                                -- use `Odd n -> 0 < n`to close the case

The only was required - it was simplifying to ¬Even n very eagerly.

I guess I've learned a whole new chunk of mathlib exists today :D