modeq

Stream: new members

[Scott Morrison]

Reasonable proof of lemma foo {k : ℕ} (h : k ≡ 1 [MOD 2]) : k ≡ 1 [MOD 4] ∨ k ≡ 3 [MOD 4] := and similar?

[Scott Morrison]

I guess

@[simp] lemma modeq_add_self (a b n : ℕ) : (a + n ≡ b [MOD n]) ↔ (a ≡ b [MOD n]) := sorry

lemma foo : Π {k : ℕ} (h : k ≡ 1 [MOD 2]), k ≡ 1 [MOD 4] ∨ k ≡ 3 [MOD 4]
| 0 h := by cases h
| 1 h := or.inl rfl
| 2 h := by cases h
| 3 h := or.inr rfl
| (n+4) h :=
begin
  rw modeq_add_self,
  erw modeq_add_self at h,
  erw modeq_add_self at h,
  exact foo h
end

works. Anything better?