proposition: Lemma same_true n P Q : same_bool n P Q = true -> forall i, i < n -> P i = Q i.
proof: Proof. induction n; intros E i L. impossible. simpl in E. auto_if; dumb. destruct (eq_nat_dec i n); dumb. apply Bool.eqb_true_iff. subst; dumb. Qed.
imports: ZArith Lia MyNat