proposition: Lemma lop_compare_sym : forall x y, lop_compare y x = CompOpp (lop_compare x y).
proof: Proof. destruct x,y; reflexivity. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause