coercion ninj.
-interpretation "zero (non-negative integers" 'Zero = nzero.
+interpretation
+ "zero (non-negative integers)"
+ 'Zero = nzero.
(* Basic inversions *********************************************************)
(* Basic constructions ******************************************************)
+(*** eq_nat_dec *)
lemma eq_nat_dec (n1,n2:nat): Decidable (n1 = n2).
* [| #p1 ] * [2,4: #p2 ]
[1,4: @or_intror #H destruct