proposition: Theorem leb_total : forall a1 a2, leb a1 a2 = true \/ leb a2 a1 = true.
proof: Proof. cbv [leb ltb]; intros a1 a2. repeat first [ rewrite !Bool.andb_true_iff | rewrite !Bool.orb_true_iff | rewrite !Z.eqb_eq | rewrite !Z.ltb_lt | rewrite !Z.leb_le ]. lia. Qed.
imports: Coq.QArith.QArith Coq.Structures.Orders Coq.micromega.Lia Coq.Bool.Bool Coq.Sorting.Mergesort Coq.Lists.List Coq.ZArith.ZArith PerformanceExperiments.Sandbox