proposition: Theorem Qpositive_le_antisym : forall w w' : Qpositive, Qpositive_le w w' -> Qpositive_le w' w -> w = w'.
proof: Proof. intros w; elim w; unfold Qpositive_le in |- *; simpl in |- *. intros w0 Hrec w'; case w'; simpl in |- *. 3: intros H; discriminate H. intros; apply f_equal with (f := nR); auto. intros w'0 H; discriminate H. intros w0 Hrec w'; case w'; simpl in |- *. 3: intros H H1; discriminate H1. intros w'1 H H1; discriminate H1. intros; apply f_equal with (f := dL); auto. intros w'; case w'; auto with *. intros w'0 H H1; discriminate H1. intros w'0 H; discriminate H. Qed.