proposition: Lemma pos_compare_eq : forall a b, pos_compare a b = true -> a = b.
proof: Proof. intro a. induction a; intros; induction b; try reflexivity. assert (false=true). assumption. discriminate H0. assert (false=true). assumption. discriminate H0. assert (false=true). assumption. discriminate H0. assert (pos_compare a b = true). assumption. rewrite (IHa _ H0). reflexivity. assert (false=true). assumption. discriminate H0. assert (false=true). assumption. discriminate H0. assert (false=true). assumption. discriminate H0. assert (pos_compare a b = true). assumption. rewrite (IHa _ H0). reflexivity. Qed.