proposition: Lemma relation_sum : forall r : Datatypes.comparison, {r = Datatypes.Eq} + {r = Datatypes.Lt} + {r = Datatypes.Gt}.
proof: Proof. intro r. elim r. left; left; reflexivity. left; right; reflexivity. right; reflexivity. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps)