proposition: Lemma Zcompare_elim : forall (c1 c2 c3:Prop) (n m:Z), (n = m -> c1) -> (n < m -> c2) -> (n > m -> c3) -> match n ?= m with | Eq => c1 | Lt => c2 | Gt => c3 end.
proof: Proof. intros. case Z.compare_spec; trivial. now Z.swap_greater. Qed.
imports: BinPos BinInt