proposition: Lemma Zcompare_rect (P:Type) (n m:Z) : ((n ?= m) = Eq -> P) -> ((n ?= m) = Lt -> P) -> ((n ?= m) = Gt -> P) -> P.
proof: Proof. intros H1 H2 H3. destruct (n ?= m); auto. Defined.
imports: Sumbool BinInt Zorder Zcompare