proposition: Lemma same_false n P Q : same_bool n P Q = false -> { i | i < n /\ P i <> Q i }.
proof: Proof. induction n; simpl; intros I. impossible. remember (Bool.eqb (P n) (Q n)) as b. destruct b. destruct IHn as (i, (Li, Di)); eauto. destruct (Bool.eqb_false_iff (P n) (Q n)); eauto. Qed.
imports: ZArith Lia MyNat