induction.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

Lemma ge0 : ∀ n, 0 ≤ n.∀ n : nat, 0 ≤ n
  induction n.0 ≤ 0
n:nat
IHn:0 ≤ n
0 ≤ S n
  - (* n ← 0 *)0 ≤ 0
    constructor.
  - (* n ← S _ *)n:nat
IHn:0 ≤ n
0 ≤ S n
    exact IHn.In environment
n : nat
IHn : 0 ≤ n
The term "IHn" has type "0 ≤ n"
while it is expected to have type "0 ≤ S n".
    constructor.n:nat
IHn:0 ≤ n
0 ≤ n
    assumption.
Qed.