proposition: Lemma positive_cast_diff: forall p q, p <> q -> positive_cast p q = None.
proof: Proof. induction p as [p IHp|p IHp| ]; intros [q|q| ]; auto; intro Heq. - simpl. rewrite IHp; auto. intro H. apply Heq. rewrite H. reflexivity. - simpl. rewrite IHp; auto. intro H. apply Heq. rewrite H. reflexivity. - elim Heq. reflexivity. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList