gistfile1.txt

uncong-suc : ∀ {m n} → suc m ≡ suc n → m ≡ n
uncong-suc refl = refl

lemma-+drop : ∀ n m o → o + n ≡ o + m → n ≡ m
lemma-+drop n m zero eq = eq
lemma-+drop n m (suc o) eq = {!!}