proposition: Lemma ceqb_spec' c1 c2 : Bool.reflect ([c1] == [c2]) (ceqb c1 c2).
proof: Proof. assert (H := morph_eq CRmorph c1 c2). assert (H' := @ceqb_complete c1 c2). destruct (ceqb c1 c2); constructor. - now apply H. - intro E. specialize (H' E). discriminate. Qed.
imports: ZArith_base