proposition: Lemma order_trans : forall b1 b2 b3, order b1 b2 -> order b2 b3 -> order b1 b3.
proof: Proof. destruct b1,b2,b3; simpl; intuition congruence. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause