Oh, how I have waited for this moment! Finally, a copyleft-style project that I can actually meaningfully contribute to!

Anyway, here is a proof of the `Program fixpoint subset`

's obligations:

```
(* l'arbre ta est-il un sous-ensemble de l'arbre tb ? *)
Program Fixpoint subset (ta : tree) (tb : tree) {measure (cardinal ta + cardinal tb)} : bool :=
match ta,tb with
| Empty,_ => true
| _,Empty => false
| Fork la na ra,Fork lb nb rb =>
match na ?= nb with
| Lt => subset (Fork la na Empty) lb && subset ra tb
| Gt => subset (Fork Empty na ra) rb && subset la tb
| Eq => subset la lb && subset ra rb
end
end.
Obligation 1.
Proof.
simpl.
do 4 rewrite <- Nat.add_assoc.
do 2 apply plus_lt_compat_l.
rewrite Nat.add_comm.
rewrite Nat.add_assoc.
rewrite (Nat.add_comm (cardinal ra)).
do 2 rewrite <- Nat.add_assoc.
apply plus_lt_compat_l.
apply Nat.lt_lt_add_r.
auto.
Qed.
Obligation 2.
Proof.
simpl.
rewrite (Nat.add_comm (cardinal la + 1)).
do 2 rewrite <- Nat.add_assoc.
apply plus_lt_compat_l.
rewrite Nat.add_assoc.
rewrite (Nat.add_comm (cardinal la + 1)).
do 3 rewrite <- Nat.add_assoc.
do 2 apply plus_lt_compat_l.
apply Nat.lt_add_pos_r.
rewrite Nat.add_1_r.
apply Nat.lt_0_succ.
Qed.
Obligation 3.
Proof.
simpl.
rewrite (Nat.add_comm (_) 1); rewrite <- Nat.add_shuffle1.
rewrite Nat.add_shuffle0; rewrite (Nat.add_assoc 1).
rewrite <- (Nat.add_assoc _ (cardinal la)).
rewrite (Nat.add_comm (cardinal la)).
do 4 rewrite <- Nat.add_assoc; do 2 apply plus_lt_compat_l.
apply Nat.lt_add_pos_r.
rewrite Nat.add_1_r.
apply (Nat.lt_lt_add_l 0 (S (cardinal lb)) (cardinal la)).
apply Nat.lt_0_succ.
Qed.
Obligation 4.
Proof.
simpl.
rewrite Nat.add_shuffle0.
rewrite <- (Nat.add_assoc _ (cardinal ra)).
rewrite (Nat.add_comm (cardinal ra)); rewrite (Nat.add_assoc (cardinal _ + _)).
rewrite <- (Nat.add_assoc _ 1); rewrite (Nat.add_comm 1 (_ + _)).
do 5 rewrite <- Nat.add_assoc.
do 3 apply plus_lt_compat_l.
apply Nat.lt_add_pos_r.
rewrite Nat.add_1_l.
apply Nat.lt_0_succ.
Qed.
Obligation 5.
Proof.
simpl.
rewrite Nat.add_shuffle0; rewrite <- (Nat.add_assoc _ 1).
rewrite (Nat.add_comm 1 _); do 4 rewrite <- Nat.add_assoc.
apply plus_lt_compat_l.
apply Nat.lt_add_pos_r.
rewrite Nat.add_1_l.
apply Nat.lt_0_succ.
Qed.
Obligation 6.
Proof.
simpl.
rewrite (Nat.add_comm (_ + 1)); rewrite Nat.add_shuffle2.
apply Nat.lt_add_pos_r; rewrite (Nat.add_comm _ 1).
rewrite Nat.add_1_l; apply Nat.lt_0_succ.
Qed.
```

Mainly just a bit of number pushing, nothing really fancy here, and Iām pretty sure there is probably a nicer way of writing this (omega?).

Naturally, CC-BY-SA.