proposition: Lemma binnat_lt_trans : forall n1 n2 n3, BinNat.N.compare n1 n2 = Lt -> BinNat.N.compare n2 n3 = Lt -> BinNat.N.compare n1 n3 = Lt.
proof: Proof. intros n1 n2 n3. zify. itauto lia_congr. Qed.
imports: ZArith Lia ZifyClasses Cdcl.Itauto