proof n≤1⇒n≡0∨n≡1

[Akshobhya1234]

From issue #1334

[Taneb]

I'm not quite convinced this property stands on its own. I think I'd like to see a use case for it. @mechvel did you have one in mind?

[mechvel]

0 and 1 are somehow more particular values in Nat than others. For example, this is so in the area of divisibility reasoning.
if n = 0 then n is divisible by everything, if n = 1 then n divides everything.
So, in divisibility reasoning one often has to check these two extreme cases. And one has to implement basic logical dependencies between the properties n ≤ 1, n ≰ 1, n ≡ 0, n ∣ 1, n ∤ 1.
The lemma n≤1⇒n≡0∨n≡1 helps this.
But in my library I use it only once:

...
n≰1 = \n≤1 → case n≤1⇒n≡0∨n≡1 n≤1                                           
                    of \      
                    { (inj₁ n≡0) → n≢0 n≡0                                        
                    ; (inj₂ n≡1) → let 1≡1*n = sym (trans (1* n) n≡1)             
                                          in  n∤1 (1 , 1≡1*n)                           
                    }       

And currently I am not so sure that this lemma is really usable.

[MatthewDaggitt]

I'm happy with accepting this. Apologies for the delay in replying.