Require Import Bool.
Require Import Sumbool.
Require Import ZArith.

Fixpoint ad_eq_1 (p1 p2:positive) {struct p2} : bool :=
match p1, p2 with
| xH, xH => true
| xO p'1, xO p'2 => ad_eq_1 p'1 p'2
| xI p'1, xI p'2 => ad_eq_1 p'1 p'2
| _, _ => false
end.

match a, a' with
| _, _ => false
end.

Proof.
destruct a; trivial.
induction p; trivial.
Qed.

Proof.
destruct a. destruct a'; trivial. destruct p.
discriminate 1.
discriminate 1.
discriminate 1.
destruct a'. intros. discriminate H.
unfold ad_eq in |- *. intros. cut (p = p0). intros. rewrite H0. reflexivity.
generalize dependent p0.
induction p as [p IHp| p IHp| ]. destruct p0; intro H.
rewrite (IHp p0). reflexivity.
exact H.
discriminate H.
discriminate H.
destruct p0; intro H. discriminate H.
rewrite (IHp p0 H). reflexivity.
discriminate H.
destruct p0 as [p| p| ]; intro H. discriminate H.
discriminate H.
trivial.
Qed.

Proof.
intros. cut (forall b b':bool, ad_eq a a' = b -> ad_eq a' a = b' -> b = b').
intros. apply H. reflexivity.
reflexivity.
destruct b. intros. cut (a = a').
intro. rewrite H1 in H0. rewrite (ad_eq_correct a') in H0. exact H0.
destruct b'. intros. cut (a' = a).
intro. rewrite H1 in H. rewrite H1 in H0. rewrite <- H. exact H0.
trivial.
Qed.

Proof.
Qed.

Proof.
intros. elim (sumbool_of_bool (ad_eq a a')). intro H0.
rewrite (ad_eq_complete a a' H0) in H. rewrite (ad_xor_nilpotent a') in H. discriminate H.
trivial.
Qed.

Proof.
rewrite <- (ad_eq_complete _ _ H0) in H. rewrite (ad_double_bit_0 a0) in H. discriminate H.
trivial.
Qed.

Proof.
rewrite <- (ad_eq_complete _ _ H0) in H. rewrite (ad_double_div_2 a0) in H.
rewrite (ad_eq_correct a0) in H. discriminate H.
Qed.

Proof.
rewrite <- (ad_eq_complete _ _ H0) in H. rewrite (ad_double_plus_un_bit_0 a0) in H.
discriminate H.
trivial.
Qed.

Proof.
rewrite (ad_eq_complete _ _ H0) in H. rewrite (ad_double_plus_un_div_2 a0) in H.
rewrite (ad_eq_correct a0) in H. discriminate H.
Qed.

Proof.
intros. elim (sumbool_of_bool (ad_eq a a')). intro H1. rewrite (ad_eq_complete _ _ H1) in H.
rewrite H in H0. discriminate H0.
trivial.
Qed.

Proof.
intros. cut (a = a'). intros. rewrite H0. apply ad_eq_correct.
Qed.

Proof.
intros. elim (sumbool_of_bool (ad_eq a a')). intro H0.
trivial.
Qed.

Proof.
intros. apply ad_faithful. unfold eqf in |- *. destruct n.
rewrite H0. reflexivity.
Qed.

ad_eq a a' = false ->
Proof.
rewrite (ad_eq_correct a') in H. discriminate H.
trivial.
Qed.

ad_eq a a' = false ->
Proof.
intros. elim H0. intro. right. apply ad_div_bit_neq. assumption.
assumption.
intro. left. assumption.