proposition: Lemma wle_antisym x : forall y, wlt x y = false -> wlt y x = false -> x = y.
proof: Proof. induction x; intros [|?]; intros; simpl in *; try congruence. apply f_equal. eapply IHx; eassumption. Qed.
imports: Fiat.FiniteSetADTs.WordInterface