proposition: Lemma compare_sym : forall x y : t, compare y x = CompOpp (compare x y).
proof: Proof. destruct x. - destruct y; simpl;auto. apply uint_compare_sym. - destruct y; simpl;auto. rewrite lop_compare_sym. destruct (lop_compare l l1); simpl; auto. apply list_compare_sym. - destruct y; simpl;auto. rewrite uint_compare_sym. destruct (id t0 ?= id t1); simpl; auto. apply list_compare_sym. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause