proposition: Lemma uint_compare_sym : forall x y, y ?= x = CompOpp (x?= y).
proof: Proof. intros. destruct (x?= y) eqn:CMP; simpl; repeat Lib.elim_compare; lia. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause