Theorem consne0 ≪ | index | src | ≫

theorem consne0 (a b: nat): $ a : b != 0 $;

suc (a, b) != 0

a : b != 0

Axiom use