proposition: Lemma log2_prop_func : forall p q, log2_prop p q -> forall q', log2_prop p q' -> q = q'.
proof: Proof. induction 1. inversion 1. auto. congruence. inversion 1. auto. congruence. inversion 1. congruence. congruence. subst. f_equal. eapply IHlog2_prop; eauto. Qed.
imports: Coq(Lia PeanoNat) CoLoR(LogicUtil NatCompat)